1  /-
  2  Copyright (c) 2014 Microsoft Corporation. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Author: Mario Carneiro
  5  
  6  Properties of the binary representation of integers.
  7  -/
  8  import data.num.basic data.num.bitwise algebra.ordered_ring
src         └────────────┘ └──────────────┘ └──────────────────┘
  9         tactic.interactive data.int.basic data.nat.gcd
src         └────────────────┘ └────────────┘ └──────────┘
 10  
 11  namespace pos_num
 12    variables {α : Type*}
 13  
 14    @[simp] theorem cast_one [has_zero α] [has_one α] [has_add α] : ((1 : pos_num) : α) = 1 := rfl
id                               └──────┘    └─────┘    └─────┘           └─────┘            └─┘
src                              └──────┘     └─────┘     └─────┘            └─────┘             └─┘
typ                              └──────┘    └─────┘    └─────┘           └─────┘            └─┘
doc      └──┘                                                                └─────┘
 15    @[simp] theorem cast_one' [has_zero α] [has_one α] [has_add α] : (pos_num.one : α) = 1 := rfl
id                                └──────┘    └─────┘    └─────┘      └─────────┘           └─┘
src                               └──────┘     └─────┘     └─────┘       └─────────┘            └─┘
typ                               └──────┘    └─────┘    └─────┘      └─────────┘           └─┘
doc      └──┘
 16    @[simp] theorem cast_bit0 [has_zero α] [has_one α] [has_add α] (n : pos_num) : (n.bit0 : α) = _root_.bit0 n := rfl
id                                └──────┘    └─────┘    └─────┘        └─────┘     └───┘      └─────────┘     └─┘
src                               └──────┘     └─────┘     └─────┘         └─────┘      └───┘       └─────────┘      └─┘
typ                               └──────┘    └─────┘    └─────┘        └─────┘     └───┘      └─────────┘     └─┘
doc      └──┘                                                              └─────┘
 17    @[simp] theorem cast_bit1 [has_zero α] [has_one α] [has_add α] (n : pos_num) : (n.bit1 : α) = _root_.bit1 n := rfl
id                                └──────┘    └─────┘    └─────┘        └─────┘     └───┘      └─────────┘     └─┘
src                               └──────┘     └─────┘     └─────┘         └─────┘      └───┘       └─────────┘      └─┘
typ                               └──────┘    └─────┘    └─────┘        └─────┘     └───┘      └─────────┘     └─┘
doc      └──┘                                                              └─────┘
 18  
 19    @[simp] theorem cast_to_nat [add_monoid α] [has_one α] : ∀ n : pos_num, ((n : ℕ) : α) = n
id                                  └────────┘    └─────┘          └─────┘              
src                                 └────────┘     └─────┘            └─────┘               
typ                                 └────────┘    └─────┘          └─────┘              
doc      └──┘                                                         └─────┘
 20    | 1        := nat.cast_one
id                   └──────────┘
src                  └──────────┘
typ                  └──────────┘
 21    | (bit0 p) := (nat.cast_bit0 _).trans $ congr_arg _root_.bit0 p.cast_to_nat
id        └──┘       └───────────┘   └───┘    └───────┘ └─────────┘
src       └──┘        └───────────┘   └───┘    └───────┘ └─────────┘
typ       └──┘       └───────────┘   └───┘    └───────┘ └─────────┘
 22    | (bit1 p) := (nat.cast_bit1 _).trans $ congr_arg _root_.bit1 p.cast_to_nat
id        └──┘       └───────────┘   └───┘    └───────┘ └─────────┘
src       └──┘        └───────────┘   └───┘    └───────┘ └─────────┘
typ       └──┘       └───────────┘   └───┘    └───────┘ └─────────┘
 23  
 24    @[simp] theorem to_nat_to_int (n : pos_num) : ((n : ℕ) : ℤ) = n :=
id                                        └─────┘                
src                                       └─────┘                
typ                                       └─────┘                
doc      └──┘                             └─────┘
 25    by rw [← int.nat_cast_eq_coe_nat, cast_to_nat]
id              └─────────────────────┘  └─────────┘
src       └────┘└─────────────────────┘└┘└─────────┘└─
typ       └────┘└─────────────────────┘└┘└─────────┘└─
doc       └────┘                       └┘           └─
txt       └────┘                       └┘           └─
par       └────┘                       └┘           └─
pid         └──┘                       └┘           
st       └────────────────────────────┘└───────────┘
 26  
src  
typ  
doc  
txt  
par  
pid  
st   
 27    @[simp] theorem cast_to_int [add_group α] [has_one α] (n : pos_num) : ((n : ℤ) : α) = n :=
id                                  └───────┘    └─────┘        └─────┘                
src  ─┘                             └───────┘     └─────┘         └─────┘                 
typ  ─┘                             └───────┘    └─────┘        └─────┘                
doc  ─┘  └──┘                                                     └─────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
 28    by rw [← to_nat_to_int, int.cast_coe_nat, cast_to_nat]
id              └───────────┘  └──────────────┘  └─────────┘
src       └────┘└───────────┘└┘└──────────────┘└┘└─────────┘└─
typ       └────┘└───────────┘└┘└──────────────┘└┘└─────────┘└─
doc       └────┘             └┘                └┘           └─
txt       └────┘             └┘                └┘           └─
par       └────┘             └┘                └┘           └─
pid         └──┘             └┘                └┘           
st       └──────────────────┘└────────────────┘└───────────┘
 29  
src  
typ  
doc  
txt  
par  
pid  
st   
 30    theorem succ_to_nat : ∀ n, (succ n : ℕ) = n + 1
id                                └──┘        
src  ─┘                            └──┘          
typ  ─┘                           └──┘        
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
 31    | 1        := rfl
id                   └─┘
src                  └─┘
typ                  └─┘
 32    | (bit0 p) := rfl
id        └──┘       └─┘
src       └──┘       └─┘
typ       └──┘       └─┘
 33    | (bit1 p) := (congr_arg _root_.bit0 (succ_to_nat p)).trans $
id        └──┘       └───────┘ └─────────┘  └─────────┘    └───┘
src       └──┘        └───────┘ └─────────┘                 └───┘
typ       └──┘       └───────┘ └─────────┘  └─────────┘    └───┘
 34      show ↑p + 1 + ↑p + 1 = ↑p + ↑p + 1 + 1, by simp
id                                
src                                      └────
typ                                      └────
doc                                                 └────
txt                                                 └────
par                                                 └────
pid                                                     
st                                                 └─────
 35  
src  
typ  
doc  
txt  
par  
pid  
st   
 36    theorem one_add (n : pos_num) : 1 + n = succ n := by cases n; refl
id                          └─────┘         └──┘              
src  ─┘                     └─────┘          └──┘         └────┘   └────
typ  ─┘                     └─────┘         └──┘        └────┘  └────
doc  ─┘                     └─────┘                         └────┘   └────
txt  ─┘                                                     └────┘   └────
par  ─┘                                                     └────┘   └────
pid  ─┘                                                                 
st   ─┘                                                    └──────────────
 37    theorem add_one (n : pos_num) : n + 1 = succ n := by cases n; refl
id                          └─────┘         └──┘              
src  ─┘                     └─────┘          └──┘         └────┘   └────
typ  ─┘                     └─────┘         └──┘        └────┘  └────
doc  ─┘                     └─────┘                         └────┘   └────
txt  ─┘                                                     └────┘   └────
par  ─┘                                                     └────┘   └────
pid  ─┘                                                                 
st   ─┘                                                    └──────────────
 38  
src  
typ  
doc  
txt  
par  
pid  
st   
 39    @[simp] theorem add_to_nat : ∀ m n, ((m + n : pos_num) : ℕ) = m + n
id                                              └─────┘         
src  ─┘                                             └─────┘         
typ  ─┘                                         └─────┘         
doc  ─┘  └──┘                                        └─────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
 40    | 1        b        := by rw [one_add b, succ_to_nat, add_comm]; refl
id                                   └─────┘   └─────────┘  └──────┘
src                              └──┘└─────┘ └┘└─────────┘└┘└──────┘  └────
typ                              └──┘└─────┘└┘└─────────┘└┘└──────┘  └────
doc                              └──┘        └┘           └┘          └────
txt                              └──┘        └┘           └┘          └────
par                              └──┘        └┘           └┘          └────
pid                                └┘        └┘           └┘              
st                              └────────────┘└───────────┘└────────┘└──────
 41    | a        1        := by rw [add_one a, succ_to_nat]; refl
id                                   └─────┘   └─────────┘
src  ─┘                          └──┘└─────┘ └┘└─────────┘  └────
typ  ─┘                          └──┘└─────┘└┘└─────────┘  └────
doc  ─┘                          └──┘        └┘             └────
txt  ─┘                          └──┘        └┘             └────
par  ─┘                          └──┘        └┘             └────
pid  ─┘                            └┘        └┘                 
st   ─┘                         └────────────┘└───────────┘└──────
 42    | (bit0 a) (bit0 b) := (congr_arg _root_.bit0 (add_to_nat a b)).trans $
id                └──┘       └───────┘ └─────────┘  └────────┘      └───┘
src  ─┘            └──┘        └───────┘ └─────────┘                  └───┘
typ  ─┘           └──┘       └───────┘ └─────────┘  └────────┘      └───┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
 43      show ((a + b) + (a + b) : ℕ) = (a + a) + (b + b), by simp
id                                            
src                                                   └────
typ                                                   └────
doc                                                           └────
txt                                                           └────
par                                                           └────
pid                                                               
st                                                           └─────
 44    | (bit0 a) (bit1 b) := (congr_arg _root_.bit1 (add_to_nat a b)).trans $
id        └──┘    └──┘       └───────┘ └─────────┘  └────────┘      └───┘
src  ─┘   └──┘     └──┘        └───────┘ └─────────┘                  └───┘
typ  ─┘   └──┘    └──┘       └───────┘ └─────────┘  └────────┘      └───┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
 45      show ((a + b) + (a + b) + 1 : ℕ) = (a + a) + (b + b + 1), by simp
id                                                  
src                                                         └────
typ                                                         └────
doc                                                                   └────
txt                                                                   └────
par                                                                   └────
pid                                                                       
st                                                                   └─────
 46    | (bit1 a) (bit0 b) := (congr_arg _root_.bit1 (add_to_nat a b)).trans $
id        └──┘    └──┘       └───────┘ └─────────┘  └────────┘      └───┘
src  ─┘   └──┘     └──┘        └───────┘ └─────────┘                  └───┘
typ  ─┘   └──┘    └──┘       └───────┘ └─────────┘  └────────┘      └───┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
 47      show ((a + b) + (a + b) + 1 : ℕ) = (a + a + 1) + (b + b), by simp
id                                                  
src                                                         └────
typ                                                         └────
doc                                                                   └────
txt                                                                   └────
par                                                                   └────
pid                                                                       
st                                                                   └─────
 48    | (bit1 a) (bit1 b) :=
id                └──┘ 
src  ─┘            └──┘
typ  ─┘           └──┘ 
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
 49      show (succ (a + b) + succ (a + b) : ℕ) = (a + a + 1) + (b + b + 1),
id             └──┘         └──┘                              
src            └──┘         └──┘                              
typ            └──┘         └──┘                              
 50      by rw [succ_to_nat, add_to_nat]; simp
id              └─────────┘  └────────┘
src         └──┘└─────────┘└┘            └────
typ         └──┘└─────────┘└┘└────────┘  └────
doc         └──┘           └┘            └────
txt         └──┘           └┘            └────
par         └──┘           └┘            └────
pid           └┘           └┘                
st         └──────────────┘└──────────┘└──────
 51  
src  
typ  
doc  
txt  
par  
pid  
st   
 52    theorem add_succ : ∀ (m n : pos_num), m + succ n = succ (m + n)
id                                └─────┘     └──┘   └──┘    
src  ─┘                            └─────┘      └──┘    └──┘    
typ  ─┘                           └─────┘     └──┘   └──┘    
doc  ─┘                            └─────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
 53    | 1        b        := by simp [one_add]
id                                     └─────┘
src                              └────┘└─────┘└─
typ                              └────┘└─────┘└─
doc                              └────┘       └─
txt                              └────┘       └─
par                              └────┘       └─
pid                                         
st                              └───────────────
 54    | (bit0 a) 1        := congr_arg bit0 (add_one a)
id        └──┘               └───────┘ └──┘  └─────┘
src  ─┘   └──┘                └───────┘ └──┘  └─────┘
typ  ─┘   └──┘               └───────┘ └──┘  └─────┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
 55    | (bit1 a) 1        := congr_arg bit1 (add_one a)
id        └──┘               └───────┘ └──┘  └─────┘
src       └──┘                └───────┘ └──┘  └─────┘
typ       └──┘               └───────┘ └──┘  └─────┘
 56    | (bit0 a) (bit0 b) := rfl
id                 └──┘       └─┘
src                └──┘       └─┘
typ                └──┘       └─┘
 57    | (bit0 a) (bit1 b) := congr_arg bit0 (add_succ a b)
id        └──┘    └──┘      └───────┘ └──┘  └──────┘
src       └──┘     └──┘       └───────┘ └──┘
typ       └──┘    └──┘      └───────┘ └──┘  └──────┘
 58    | (bit1 a) (bit0 b) := rfl
id        └──┘     └──┘       └─┘
src       └──┘     └──┘       └─┘
typ       └──┘     └──┘       └─┘
 59    | (bit1 a) (bit1 b) := congr_arg bit1 (add_succ a b)
id                └──┘      └───────┘ └──┘  └──────┘
src                └──┘       └───────┘ └──┘
typ               └──┘      └───────┘ └──┘  └──────┘
 60  
 61    theorem bit0_of_bit0 : Π n, _root_.bit0 n = bit0 n
id                                └─────────┘   └──┘ 
src                                └─────────┘    └──┘
typ                               └─────────┘   └──┘ 
 62    | 1        := rfl
id                   └─┘
src                  └─┘
typ                  └─┘
 63    | (bit0 p) := congr_arg bit0 (bit0_of_bit0 p)
id        └──┘      └───────┘ └──┘  └──────────┘
src       └──┘       └───────┘ └──┘
typ       └──┘      └───────┘ └──┘  └──────────┘
 64    | (bit1 p) := show bit0 (succ (_root_.bit0 p)) = _, by rw bit0_of_bit0; refl
id        └──┘           └──┘  └──┘  └─────────┘               └──────────┘
src       └──┘            └──┘  └──┘  └─────────┘            └─┘              └────
typ       └──┘           └──┘  └──┘  └─────────┘            └─┘└──────────┘  └────
doc                                                           └─┘              └────
txt                                                           └─┘              └────
par                                                           └─┘              └────
pid                                                                               
st                                                           └──────────────────────
 65  
src  
typ  
doc  
txt  
par  
pid  
st   
 66    theorem bit1_of_bit1 (n : pos_num) : _root_.bit1 n = bit1 n :=
id                               └─────┘    └─────────┘   └──┘ 
src  ─┘                          └─────┘    └─────────┘    └──┘
typ  ─┘                          └─────┘    └─────────┘   └──┘ 
doc  ─┘                          └─────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
 67    show _root_.bit0 n + 1 = bit1 n, by rw [add_one, bit0_of_bit0]; refl
id          └─────────┘      └──┘          └─────┘  └──────────┘
src         └─────────┘       └──┘       └──┘└─────┘└┘└──────────┘  └────
typ         └─────────┘      └──┘      └──┘└─────┘└┘└──────────┘  └────
doc                                        └──┘       └┘              └────
txt                                        └──┘       └┘              └────
par                                        └──┘       └┘              └────
pid                                          └┘       └┘                  
st                                        └──────────┘└────────────┘└──────
 68  
src  
typ  
doc  
txt  
par  
pid  
st   
 69    @[simp] theorem mul_to_nat (m) : ∀ n, ((m * n : pos_num) : ℕ) = m * n
id                                                 └─────┘         
src  ─┘                                               └─────┘         
typ  ─┘                                            └─────┘         
doc  ─┘  └──┘                                          └─────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
 70    | 1        := (mul_one _).symm
id                    └─────┘   └──┘
src                   └─────┘   └──┘
typ                   └─────┘   └──┘
 71    | (bit0 p) := show (↑(m * p) + ↑(m * p) : ℕ) = ↑m * (p + p), by rw [mul_to_nat, left_distrib]
id        └──┘                                               └────────┘  └──────────┘
src       └──┘                                               └──┘          └┘└──────────┘└─
typ       └──┘                                           └──┘└────────┘└┘└──────────┘└─
doc                                                                    └──┘          └┘            └─
txt                                                                    └──┘          └┘            └─
par                                                                    └──┘          └┘            └─
pid                                                                      └┘          └┘            
st                                                                    └─────────────┘└────────────┘
 72    | (bit1 p) := (add_to_nat (bit0 (m * p)) m).trans $
id        └──┘       └────────┘  └──┘         └───┘
src  ─┘   └──┘        └────────┘  └──┘           └───┘
typ  ─┘   └──┘       └────────┘  └──┘         └───┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
 73      show (↑(m * p) + ↑(m * p) + ↑m : ℕ) = ↑m * (p + p) + m, by rw [mul_to_nat, left_distrib]
id                                                    └────────┘  └──────────┘
src                                                    └──┘          └┘└──────────┘└─
typ                                               └──┘└────────┘└┘└──────────┘└─
doc                                                                 └──┘          └┘            └─
txt                                                                 └──┘          └┘            └─
par                                                                 └──┘          └┘            └─
pid                                                                   └┘          └┘            
st                                                                 └─────────────┘└────────────┘
 74  
src  
typ  
doc  
txt  
par  
pid  
st   
 75    theorem to_nat_pos : ∀ n : pos_num, 0 < (n : ℕ)
id                               └─────┘         
src  ─┘                           └─────┘          
typ  ─┘                          └─────┘         
doc  ─┘                           └─────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
 76    | 1        := zero_lt_one
id                   └─────────┘
src                  └─────────┘
typ                  └─────────┘
 77    | (bit0 p) := let h := to_nat_pos p in add_pos h h
id        └──┘              └────────┘      └─────┘  
src       └──┘                                └─────┘
typ       └──┘              └────────┘      └─────┘  
 78    | (bit1 p) := nat.succ_pos _
id        └──┘       └──────────┘
src       └──┘       └──────────┘
typ       └──┘       └──────────┘
 79  
 80    theorem cmp_to_nat_lemma {m n : pos_num} : (m:ℕ) < n → (bit1 m : ℕ) < bit0 n :=
id                                     └─────┘             └──┘       └──┘ 
src                                    └─────┘               └──┘        └──┘
typ                                    └─────┘             └──┘       └──┘ 
doc                                    └─────┘
 81    show (m:ℕ) < n → (m + m + 1 + 1 : ℕ) ≤ n + n,
id                                  
src                                      
typ                                 
 82    by intro h; rw [nat.add_right_comm m m 1, add_assoc]; exact add_le_add h h
id                     └────────────────┘       └───────┘         └────────┘   
src       └─────┘  └──┘└────────────────┘  └──┘└───────┘  └────┘└────────┘  
typ       └─────┘  └──┘└────────────────┘ └──┘└───────┘  └────┘└────────┘ 
doc       └─────┘  └──┘                    └──┘           └────┘            
txt       └─────┘  └──┘                    └──┘           └────┘            
par       └─────┘  └──┘                    └──┘           └────┘            
pid            └┘    └┘                    └──┘                            
st       └────────────┘└─────────────────────┘└──────────┘└──────────────────────
 83  
src  
typ  
doc  
txt  
par  
pid  
st   
 84    theorem cmp_swap (m) : ∀n, (cmp m n).swap = cmp n m :=
id                                └─┘   └──┘   └─┘  
src  ─┘                            └─┘     └──┘   └─┘
typ  ─┘                           └─┘   └──┘   └─┘  
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
 85    by induction m with m IH m IH; intro n;
id                  
src       └────────┘ └─────────────┘  └─────┘
typ       └────────┘└─────────────┘  └─────┘
doc       └────────┘ └─────────────┘  └─────┘
txt       └────────┘ └─────────────┘  └─────┘
par       └────────┘ └─────────────┘  └─────┘
pid                 └────────────┘       └┘
st       └─────────────────────────────────────
 86       cases n with n n; try {unfold cmp}; try {refl}; rw ←IH; cases cmp m n; refl
id                                                           └┘        └─┘  
src       └────┘ └───────┘  └───┘└────────┘  └───┘└──┘  └──┘    └────┘└─┘    └────
typ       └────┘└───────┘  └───┘└────────┘  └───┘└──┘  └──┘└┘  └────┘└─┘  └────
doc       └────┘ └───────┘  └───┘└────────┘  └───┘└──┘  └──┘    └────┘       └────
txt       └────┘ └───────┘  └───┘└────────┘  └───┘└──┘  └──┘    └────┘       └────
par       └────┘ └───────┘  └───┘└────────┘  └───┘└──┘  └──┘    └────┘       └────
pid             └───────┘     └───────────┘     └─────┘    └┘                    
st   ───────────────────────────┘└────────┘└┘└────┘└──┘└┘└────────────────────────────
 87  
src  
typ  
doc  
txt  
par  
pid  
st   
 88    theorem cmp_to_nat : ∀ (m n), (ordering.cases_on (cmp m n) ((m:ℕ) < n) (m = n) ((m:ℕ) > n) : Prop)
id                                 └───────────────┘  └─┘                       
src  ─┘                               └───────────────┘  └─┘                             
typ  ─┘                            └───────────────┘  └─┘                       
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
 89    | 1        1        := rfl
id                            └─┘
src                           └─┘
typ                           └─┘
 90    | (bit0 a) 1        := let h : (1:ℕ) ≤ a := to_nat_pos a in add_le_add h h
id        └──┘                                  └────────┘      └────────┘  
src       └──┘                                   └────────┘      └────────┘
typ       └──┘                                  └────────┘      └────────┘  
 91    | (bit1 a) 1        := nat.succ_lt_succ $ to_nat_pos $ bit0 a
id        └──┘               └──────────────┘   └────────┘   └──┘
src       └──┘                └──────────────┘   └────────┘   └──┘
typ       └──┘               └──────────────┘   └────────┘   └──┘
 92    | 1        (bit0 b) := let h : (1:ℕ) ≤ b := to_nat_pos b in add_le_add h h
id                 └──┘                         └────────┘      └────────┘  
src                └──┘                          └────────┘      └────────┘
typ                └──┘                         └────────┘      └────────┘  
 93    | 1        (bit1 b) := nat.succ_lt_succ $ to_nat_pos $ bit0 b
id                 └──┘      └──────────────┘   └────────┘   └──┘
src                └──┘       └──────────────┘   └────────┘   └──┘
typ                └──┘      └──────────────┘   └────────┘   └──┘
 94    | (bit0 a) (bit0 b) := begin
id                 └──┘
src                └──┘
typ                └──┘
st                            └─────
 95        have := cmp_to_nat a b, revert this, cases cmp a b; dsimp; intro,
id                 └────────┘                       └─┘  
src        └──────┘              └─────────┘  └────┘└─┘    └───┘  └───┘
typ        └──────┘└────────┘  └─────────┘  └────┘└─┘  └───┘  └───┘
doc        └──────┘              └─────────┘  └────┘       └───┘  └───┘
txt        └──────┘              └─────────┘  └────┘       └───┘  └───┘
par        └──────┘              └─────────┘  └────┘       └───┘  └───┘
pid        └───┘└─┘                    └───┘           
st   ───────────────────────────┘└───────────┘└───────────────────────────┘└─
 96        { exact add_lt_add this this },
id                 └────────┘      └──┘
src          └────┘└────────┘        
typ          └────┘└────────┘    └──┘
doc          └────┘                  
txt          └────┘                  
par          └────┘                  
pid                                 
st   ───────┘└─────────────────────────┘└┘
 97        { rw this },
id              └──┘
src          └─┘    
typ          └─┘└──┘
doc          └─┘    
txt          └─┘    
par          └─┘    
pid                
st   ───────┘└──────┘└┘
 98        { exact add_lt_add this this }
id                 └────────┘      └──┘
src          └────┘└────────┘        
typ          └────┘└────────┘    └──┘
doc          └────┘                  
txt          └────┘                  
par          └────┘                  
pid                                 
st   ──────────────────────────────────┘└─
 99      end
st   ──────┘
100    | (bit0 a) (bit1 b) := begin dsimp [cmp],
id        └──┘     └──┘                    └─┘
src       └──┘     └──┘             └─────┘└─┘
typ       └──┘     └──┘             └─────┘└─┘
doc                                 └─────┘   
txt                                 └─────┘   
par                                 └─────┘   
pid                                         
st                            └───────────────┘└─
101        have := cmp_to_nat a b, revert this, cases cmp a b; dsimp; intro,
id                 └────────┘                       └─┘  
src        └──────┘              └─────────┘  └────┘└─┘    └───┘  └───┘
typ        └──────┘└────────┘  └─────────┘  └────┘└─┘  └───┘  └───┘
doc        └──────┘              └─────────┘  └────┘       └───┘  └───┘
txt        └──────┘              └─────────┘  └────┘       └───┘  └───┘
par        └──────┘              └─────────┘  └────┘       └───┘  └───┘
pid        └───┘└─┘                    └───┘           
st   ───────────────────────────┘└───────────┘└───────────────────────────┘└─
102        { exact nat.le_succ_of_le (add_lt_add this this) },
id                 └───────────────┘  └────────┘      └──┘
src          └────┘└───────────────┘ └────────┘        └┘
typ          └────┘└───────────────┘ └────────┘    └──┘└┘
doc          └────┘                                    └┘
txt          └────┘                                    └┘
par          └────┘                                    └┘
pid                                                   
st   ───────┘└─────────────────────────────────────────────┘└┘
103        { rw this, apply nat.lt_succ_self },
id              └──┘        └──────────────┘
src          └─┘      └────┘└──────────────┘
typ          └─┘└──┘  └────┘└──────────────┘
doc          └─┘      └────┘                
txt          └─┘      └────┘                
par          └─┘      └────┘                
pid                                       
st   ───────┘└─────┘└───────────────────────┘└┘
104        { exact cmp_to_nat_lemma this }
id                 └──────────────┘ └──┘
src          └────┘└──────────────┘    
typ          └────┘└──────────────┘└──┘
doc          └────┘                    
txt          └────┘                    
par          └────┘                    
pid                                   
st   ───────────────────────────────────┘└─
105      end
st   ──────┘
106    | (bit1 a) (bit0 b) := begin dsimp [cmp],
id        └──┘     └──┘                    └─┘
src       └──┘     └──┘             └─────┘└─┘
typ       └──┘     └──┘             └─────┘└─┘
doc                                 └─────┘   
txt                                 └─────┘   
par                                 └─────┘   
pid                                         
st                            └───────────────┘└─
107        have := cmp_to_nat a b, revert this, cases cmp a b; dsimp; intro,
id                 └────────┘                       └─┘  
src        └──────┘              └─────────┘  └────┘└─┘    └───┘  └───┘
typ        └──────┘└────────┘  └─────────┘  └────┘└─┘  └───┘  └───┘
doc        └──────┘              └─────────┘  └────┘       └───┘  └───┘
txt        └──────┘              └─────────┘  └────┘       └───┘  └───┘
par        └──────┘              └─────────┘  └────┘       └───┘  └───┘
pid        └───┘└─┘                    └───┘           
st   ───────────────────────────┘└───────────┘└───────────────────────────┘└─
108        { exact cmp_to_nat_lemma this },
id                 └──────────────┘ └──┘
src          └────┘└──────────────┘    
typ          └────┘└──────────────┘└──┘
doc          └────┘                    
txt          └────┘                    
par          └────┘                    
pid                                   
st   ───────┘└──────────────────────────┘└┘
109        { rw this, apply nat.lt_succ_self },
id              └──┘        └──────────────┘
src          └─┘      └────┘└──────────────┘
typ          └─┘└──┘  └────┘└──────────────┘
doc          └─┘      └────┘                
txt          └─┘      └────┘                
par          └─┘      └────┘                
pid                                       
st   ───────┘└─────┘└───────────────────────┘└┘
110        { exact nat.le_succ_of_le (add_lt_add this this) },
id                 └───────────────┘  └────────┘      └──┘
src          └────┘└───────────────┘ └────────┘        └┘
typ          └────┘└───────────────┘ └────────┘    └──┘└┘
doc          └────┘                                    └┘
txt          └────┘                                    └┘
par          └────┘                                    └┘
pid                                                   
st   ──────────────────────────────────────────────────────┘└──
111      end
st   ──────┘
112    | (bit1 a) (bit1 b) := begin
id                 └──┘
src                └──┘
typ                └──┘
st                            └─────
113        have := cmp_to_nat a b, revert this, cases cmp a b; dsimp; intro,
id                 └────────┘                       └─┘  
src        └──────┘              └─────────┘  └────┘└─┘    └───┘  └───┘
typ        └──────┘└────────┘  └─────────┘  └────┘└─┘  └───┘  └───┘
doc        └──────┘              └─────────┘  └────┘       └───┘  └───┘
txt        └──────┘              └─────────┘  └────┘       └───┘  └───┘
par        └──────┘              └─────────┘  └────┘       └───┘  └───┘
pid        └───┘└─┘                    └───┘           
st   ───────────────────────────┘└───────────┘└───────────────────────────┘└─
114        { exact nat.succ_lt_succ (add_lt_add this this) },
id                 └──────────────┘  └────────┘      └──┘
src          └────┘└──────────────┘ └────────┘        └┘
typ          └────┘└──────────────┘ └────────┘    └──┘└┘
doc          └────┘                                   └┘
txt          └────┘                                   └┘
par          └────┘                                   └┘
pid                                                  
st   ───────┘└────────────────────────────────────────────┘└┘
115        { rw this },
id              └──┘
src          └─┘    
typ          └─┘└──┘
doc          └─┘    
txt          └─┘    
par          └─┘    
pid                
st   ───────┘└──────┘└┘
116        { exact nat.succ_lt_succ (add_lt_add this this) }
id                 └──────────────┘  └────────┘      └──┘
src          └────┘└──────────────┘ └────────┘        └┘
typ          └────┘└──────────────┘ └────────┘    └──┘└┘
doc          └────┘                                   └┘
txt          └────┘                                   └┘
par          └────┘                                   └┘
pid                                                  
st   ─────────────────────────────────────────────────────┘└─
117      end
st   ──────┘
118  
119    @[simp] theorem lt_to_nat {m n : pos_num} : (m:ℕ) < n ↔ m < n :=
id                                      └─────┘             
src                                     └─────┘               
typ                                     └─────┘             
doc      └──┘                           └─────┘
120    show (m:ℕ) < n ↔ cmp m n = ordering.lt, from
id                 └─┘    └─────────┘
src                  └─┘      └─────────┘
typ                └─┘    └─────────┘
121    match cmp m n, cmp_to_nat m n with
id           └─┘    └────────┘  
src          └─┘      └────────┘
typ          └─┘    └────────┘  
122    | ordering.lt, h := by simp at h; simp [h]
id       └─────────┘                           
src      └─────────┘          └───────┘  └────┘ └─
typ      └─────────┘          └───────┘  └────┘└─
doc                           └───────┘  └────┘ └─
txt                           └───────┘  └────┘ └─
par                           └───────┘  └────┘ └─
pid                               └──┘       
st                           └────────────────────
123    | ordering.eq, h := by simp at h; simp [h, lt_irrefl]; exact dec_trivial
id       └─────────┘                             └───────┘
src  ─┘  └─────────┘          └───────┘  └────┘ └┘└───────┘  └────┘           
typ  ─┘  └─────────┘          └───────┘  └────┘└┘└───────┘  └────┘           
doc  ─┘                       └───────┘  └────┘ └┘           └────┘           
txt  ─┘                       └───────┘  └────┘ └┘           └────┘           
par  ─┘                       └───────┘  └────┘ └┘           └────┘           
pid  ─┘                           └──┘       └┘                           
st   ─┘                      └──────────────────────────────────────────────────
124    | ordering.gt, h := by simp [not_lt_of_gt h]; exact dec_trivial
id       └─────────┘                └──────────┘ 
src  ─┘  └─────────┘          └────┘└──────────┘   └────┘           
typ  ─┘  └─────────┘          └────┘└──────────┘  └────┘           
doc  ─┘                       └────┘               └────┘           
txt  ─┘                       └────┘               └────┘           
par  ─┘                       └────┘               └────┘           
pid  ─┘                                                          
st   ─┘                      └─────────────────────────────────────────
125    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
126  
127    @[simp] theorem le_to_nat {m n : pos_num} : (m:ℕ) ≤ n ↔ m ≤ n :=
id                                      └─────┘             
src                                     └─────┘               
typ                                     └─────┘             
doc      └──┘                           └─────┘
128    by rw ← not_lt; exact not_congr lt_to_nat
id             └────┘        └───────┘ └───────┘
src       └───┘└────┘  └────┘└───────┘└───────┘
typ       └───┘└────┘  └────┘└───────┘└───────┘
doc       └───┘        └────┘                  
txt       └───┘        └────┘                  
par       └───┘        └────┘                  
pid         └─┘                               
st       └───────────────────────────────────────
129  
src  
typ  
doc  
txt  
par  
pid  
st   
130  end pos_num
131  
132  namespace num
133    variables {α : Type*}
134    open pos_num
135  
136    theorem add_zero (n : num) : n + 0 = n := by cases n; refl
id                           └─┘                      
src                          └─┘                  └────┘   └────
typ                          └─┘                └────┘  └────
doc                          └─┘                    └────┘   └────
txt                                                 └────┘   └────
par                                                 └────┘   └────
pid                                                             
st                                                 └──────────────
137    theorem zero_add (n : num) : 0 + n = n := by cases n; refl
id                           └─┘                      
src  ─┘                      └─┘                  └────┘   └────
typ  ─┘                      └─┘                └────┘  └────
doc  ─┘                      └─┘                    └────┘   └────
txt  ─┘                                             └────┘   └────
par  ─┘                                             └────┘   └────
pid  ─┘                                                         
st   ─┘                                            └──────────────
138  
src  
typ  
doc  
txt  
par  
pid  
st   
139    theorem add_one : ∀ n : num, n + 1 = succ n
id                            └─┘       └──┘ 
src  ─┘                        └─┘        └──┘
typ  ─┘                       └─┘       └──┘ 
doc  ─┘                        └─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
140    | 0       := rfl
id                  └─┘
src                 └─┘
typ                 └─┘
141    | (pos p) := by cases p; refl
id        └─┘                
src       └─┘          └────┘   └────
typ       └─┘          └────┘  └────
doc                    └────┘   └────
txt                    └────┘   └────
par                    └────┘   └────
pid                                
st                    └──────────────
142  
src  
typ  
doc  
txt  
par  
pid  
st   
143    theorem add_succ : ∀ (m n : num), m + succ n = succ (m + n)
id                                └─┘     └──┘   └──┘    
src  ─┘                            └─┘      └──┘    └──┘    
typ  ─┘                           └─┘     └──┘   └──┘    
doc  ─┘                            └─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
144    | 0       n       := by simp [zero_add]
id                                   └──────┘
src                            └────┘└──────┘└─
typ                            └────┘└──────┘└─
doc                            └────┘        └─
txt                            └────┘        └─
par                            └────┘        └─
pid                                        
st                            └────────────────
145    | (pos p) 0       := show pos (p + 1) = succ (pos p + 0),
id        └─┘                   └─┘         └──┘  └─┘   
src  ─┘   └─┘                    └─┘         └──┘  └─┘   
typ  ─┘   └─┘                   └─┘         └──┘  └─┘   
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
146                         by rw [pos_num.add_one, add_zero]; refl
id                                 └─────────────┘  └──────┘
src                            └──┘└─────────────┘└┘└──────┘  └────
typ                            └──┘└─────────────┘└┘└──────┘  └────
doc                            └──┘               └┘          └────
txt                            └──┘               └┘          └────
par                            └──┘               └┘          └────
pid                              └┘               └┘              
st                            └──────────────────┘└────────┘└──────
147    | (pos p) (pos q) := congr_arg pos (pos_num.add_succ _ _)
id                └─┘       └───────┘ └─┘  └──────────────┘
src  ─┘           └─┘       └───────┘ └─┘  └──────────────┘
typ  ─┘           └─┘       └───────┘ └─┘  └──────────────┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
148  
149    @[simp] theorem add_of_nat (m) : ∀ n, ((m + n : ℕ) : num) = m + n
id                                                     └─┘     
src                                                       └─┘     
typ                                                    └─┘     
doc      └──┘                                               └─┘
150    | 0     := (add_zero _).symm
id                 └──────┘   └──┘
src                └──────┘   └──┘
typ                └──────┘   └──┘
151    | (n+1) := show ((m + n : ℕ) + 1 : num) = m + (↑ n + 1),
id                                  └─┘         
src                                   └─┘          
typ                                 └─┘         
doc                                       └─┘
152               by rw [add_one, add_one, add_succ, add_of_nat]
id                       └─────┘  └─────┘  └──────┘  └────────┘
src                  └──┘└─────┘└┘└─────┘└┘└──────┘└┘          └─
typ                  └──┘└─────┘└┘└─────┘└┘└──────┘└┘└────────┘└─
doc                  └──┘       └┘       └┘        └┘          └─
txt                  └──┘       └┘       └┘        └┘          └─
par                  └──┘       └┘       └┘        └┘          └─
pid                    └┘       └┘       └┘        └┘          
st                  └──────────┘└───────┘└────────┘└──────────┘
153  
src  
typ  
doc  
txt  
par  
pid  
st   
154    theorem bit0_of_bit0 : ∀ n : num, bit0 n = n.bit0
id                                 └─┘  └──┘   └───┘
src  ─┘                             └─┘  └──┘     └───┘
typ  ─┘                            └─┘  └──┘   └───┘
doc  ─┘                             └─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
155    | 0       := rfl
id                  └─┘
src                 └─┘
typ                 └─┘
156    | (pos p) := congr_arg pos p.bit0_of_bit0
id        └─┘      └───────┘ └─┘  └───────────┘
src       └─┘       └───────┘ └─┘  └───────────┘
typ       └─┘      └───────┘ └─┘  └───────────┘
157  
158    theorem bit1_of_bit1 : ∀ n : num, bit1 n = n.bit1
id                                 └─┘  └──┘   └───┘
src                                 └─┘  └──┘     └───┘
typ                                └─┘  └──┘   └───┘
doc                                 └─┘
159    | 0       := rfl
id                  └─┘
src                 └─┘
typ                 └─┘
160    | (pos p) := congr_arg pos p.bit1_of_bit1
id        └─┘      └───────┘ └─┘  └───────────┘
src       └─┘       └───────┘ └─┘  └───────────┘
typ       └─┘      └───────┘ └─┘  └───────────┘
161  
162    @[simp] theorem cast_zero [has_zero α] [has_one α] [has_add α] :
id                                └──────┘    └─────┘    └─────┘ 
src                               └──────┘     └─────┘     └─────┘
typ                               └──────┘    └─────┘    └─────┘ 
doc      └──┘
163      ((0 : num) : α) = 0 := rfl
id             └─┘            └─┘
src            └─┘             └─┘
typ            └─┘            └─┘
doc            └─┘
164  
165    @[simp] theorem cast_zero' [has_zero α] [has_one α] [has_add α] :
id                                 └──────┘    └─────┘    └─────┘ 
src                                └──────┘     └─────┘     └─────┘
typ                                └──────┘    └─────┘    └─────┘ 
doc      └──┘
166      (num.zero : α) = 0 := rfl
id        └──────┘           └─┘
src       └──────┘            └─┘
typ       └──────┘           └─┘
167  
168    @[simp] theorem cast_one [has_zero α] [has_one α] [has_add α] :
id                               └──────┘    └─────┘    └─────┘ 
src                              └──────┘     └─────┘     └─────┘
typ                              └──────┘    └─────┘    └─────┘ 
doc      └──┘
169      ((1 : num) : α) = 1 := rfl
id             └─┘            └─┘
src            └─┘             └─┘
typ            └─┘            └─┘
doc            └─┘
170  
171    @[simp] theorem cast_pos [has_zero α] [has_one α] [has_add α]
id                               └──────┘    └─────┘    └─────┘ 
src                              └──────┘     └─────┘     └─────┘
typ                              └──────┘    └─────┘    └─────┘ 
doc      └──┘
172      (n : pos_num) : (num.pos n : α) = n := rfl
id            └─────┘     └─────┘           └─┘
src           └─────┘     └─────┘              └─┘
typ           └─────┘     └─────┘           └─┘
doc           └─────┘
173  
174    theorem succ'_to_nat : ∀ n, (succ' n : ℕ) = n + 1
id                                 └───┘        
src                                 └───┘          
typ                                └───┘        
175    | 0       := (_root_.zero_add _).symm
id                   └─────────────┘   └──┘
src                  └─────────────┘   └──┘
typ                  └─────────────┘   └──┘
176    | (pos p) := pos_num.succ_to_nat _
id        └─┘       └─────────────────┘
src       └─┘       └─────────────────┘
typ       └─┘       └─────────────────┘
177  
178    theorem succ_to_nat (n) : (succ n : ℕ) = n + 1 := succ'_to_nat n
id                                └──┘              └──────────┘ 
src                               └──┘                └──────────┘
typ                               └──┘              └──────────┘ 
179  
180    @[simp] theorem cast_to_nat [add_monoid α] [has_one α] : ∀ n : num, ((n : ℕ) : α) = n
id                                  └────────┘    └─────┘          └─┘              
src                                 └────────┘     └─────┘            └─┘               
typ                                 └────────┘    └─────┘          └─┘              
doc      └──┘                                                         └─┘
181    | 0       := nat.cast_zero
id                  └───────────┘
src                 └───────────┘
typ                 └───────────┘
182    | (pos p) := p.cast_to_nat
id        └─┘       └──────────┘
src       └─┘        └──────────┘
typ       └─┘       └──────────┘
183  
184    @[simp] theorem to_nat_to_int (n : num) : ((n : ℕ) : ℤ) = n :=
id                                        └─┘                
src                                       └─┘                
typ                                       └─┘                
doc      └──┘                             └─┘
185    by rw [← int.nat_cast_eq_coe_nat, cast_to_nat]
id              └─────────────────────┘  └─────────┘
src       └────┘└─────────────────────┘└┘└─────────┘└─
typ       └────┘└─────────────────────┘└┘└─────────┘└─
doc       └────┘                       └┘           └─
txt       └────┘                       └┘           └─
par       └────┘                       └┘           └─
pid         └──┘                       └┘           
st       └────────────────────────────┘└───────────┘
186  
src  
typ  
doc  
txt  
par  
pid  
st   
187    @[simp] theorem cast_to_int [add_group α] [has_one α] (n : num) : ((n : ℤ) : α) = n :=
id                                  └───────┘    └─────┘        └─┘                
src  ─┘                             └───────┘     └─────┘         └─┘                 
typ  ─┘                             └───────┘    └─────┘        └─┘                
doc  ─┘  └──┘                                                     └─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
188    by rw [← to_nat_to_int, int.cast_coe_nat, cast_to_nat]
id              └───────────┘  └──────────────┘  └─────────┘
src       └────┘└───────────┘└┘└──────────────┘└┘└─────────┘└─
typ       └────┘└───────────┘└┘└──────────────┘└┘└─────────┘└─
doc       └────┘             └┘                └┘           └─
txt       └────┘             └┘                └┘           └─
par       └────┘             └┘                └┘           └─
pid         └──┘             └┘                └┘           
st       └──────────────────┘└────────────────┘└───────────┘
189  
src  
typ  
doc  
txt  
par  
pid  
st   
190    @[simp] theorem to_of_nat : Π (n : ℕ), ((n : num) : ℕ) = n
id                                               └─┘       
src  ─┘                                            └─┘      
typ  ─┘                                          └─┘       
doc  ─┘  └──┘                                       └─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
191    | 0     := rfl
id                └─┘
src               └─┘
typ               └─┘
192    | (n+1) := by rw [nat.cast_add_one, add_one, succ_to_nat, to_of_nat]
id                      └──────────────┘  └─────┘  └─────────┘  └───────┘
src                 └──┘└──────────────┘└┘└─────┘└┘└─────────┘└┘         └─
typ                 └──┘└──────────────┘└┘└─────┘└┘└─────────┘└┘└───────┘└─
doc                  └──┘                └┘       └┘           └┘         └─
txt                  └──┘                └┘       └┘           └┘         └─
par                  └──┘                └┘       └┘           └┘         └─
pid                    └┘                └┘       └┘           └┘         
st                  └───────────────────┘└───────┘└───────────┘└─────────┘
193  
src  
typ  
doc  
txt  
par  
pid  
st   
194    @[simp] theorem of_nat_cast [add_monoid α] [has_one α] (n : ℕ) : ((n : num) : α) = n :=
id                                  └────────┘    └─────┘                 └─┘       
src  ─┘                             └────────┘     └─────┘                   └─┘       
typ  ─┘                             └────────┘    └─────┘                 └─┘       
doc  ─┘  └──┘                                                                 └─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
195    by rw [← cast_to_nat, to_of_nat]
id              └─────────┘  └───────┘
src       └────┘└─────────┘└┘└───────┘└─
typ       └────┘└─────────┘└┘└───────┘└─
doc       └────┘           └┘         └─
txt       └────┘           └┘         └─
par       └────┘           └┘         └─
pid         └──┘           └┘         
st       └────────────────┘└─────────┘
196  
src  
typ  
doc  
txt  
par  
pid  
st   
197    theorem of_nat_inj {m n : ℕ} : (m : num) = n ↔ m = n :=
id                                       └─┘       
src  ─┘                                   └─┘        
typ  ─┘                                  └─┘       
doc  ─┘                                    └─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
198    ⟨λ h, function.injective_of_left_inverse to_of_nat h, congr_arg _⟩
id          └────────────────────────────────┘ └───────┘   └───────┘
src          └────────────────────────────────┘ └───────┘    └───────┘
typ         └────────────────────────────────┘ └───────┘   └───────┘
199  
200    @[simp] theorem add_to_nat : ∀ m n, ((m + n : num) : ℕ) = m + n
id                                              └─┘         
src                                                 └─┘         
typ                                             └─┘         
doc      └──┘                                        └─┘
201    | 0       0       := rfl
id                          └─┘
src                         └─┘
typ                         └─┘
202    | 0       (pos q) := (_root_.zero_add _).symm
id                └─┘        └─────────────┘   └──┘
src               └─┘        └─────────────┘   └──┘
typ               └─┘        └─────────────┘   └──┘
203    | (pos p) 0       := rfl
id        └─┘               └─┘
src       └─┘               └─┘
typ       └─┘               └─┘
204    | (pos p) (pos q) := pos_num.add_to_nat _ _
id                └─┘       └────────────────┘
src               └─┘       └────────────────┘
typ               └─┘       └────────────────┘
205  
206    @[simp] theorem mul_to_nat : ∀ m n, ((m * n : num) : ℕ) = m * n
id                                              └─┘         
src                                                 └─┘         
typ                                             └─┘         
doc      └──┘                                        └─┘
207    | 0       0       := rfl
id                          └─┘
src                         └─┘
typ                         └─┘
208    | 0       (pos q) := (zero_mul _).symm
id                └─┘        └──────┘   └──┘
src               └─┘        └──────┘   └──┘
typ               └─┘        └──────┘   └──┘
209    | (pos p) 0       := rfl
id        └─┘               └─┘
src       └─┘               └─┘
typ       └─┘               └─┘
210    | (pos p) (pos q) := pos_num.mul_to_nat _ _
id                └─┘       └────────────────┘
src               └─┘       └────────────────┘
typ               └─┘       └────────────────┘
211  
212    theorem cmp_to_nat : ∀ (m n), (ordering.cases_on (cmp m n) ((m:ℕ) < n) (m = n) ((m:ℕ) > n) : Prop)
id                                 └───────────────┘  └─┘                       
src                                   └───────────────┘  └─┘                             
typ                                └───────────────┘  └─┘                       
213    | 0       0       := rfl
id                          └─┘
src                         └─┘
typ                         └─┘
214    | 0       (pos b) := to_nat_pos _
id                └─┘       └────────┘
src               └─┘       └────────┘
typ               └─┘       └────────┘
215    | (pos a) 0       := to_nat_pos _
id        └─┘               └────────┘
src       └─┘               └────────┘
typ       └─┘               └────────┘
216    | (pos a) (pos b) :=
id                └─┘
src               └─┘
typ               └─┘
217      by { have := pos_num.cmp_to_nat a b; revert this; dsimp [cmp];
id                    └────────────────┘                        └─┘
src           └──────┘└────────────────┘    └─────────┘  └─────┘└─┘
typ           └──────┘└────────────────┘  └─────────┘  └─────┘└─┘
doc           └──────┘                      └─────────┘  └─────┘   
txt           └──────┘                      └─────────┘  └─────┘   
par           └──────┘                      └─────────┘  └─────┘   
pid           └───┘└─┘                            └───┘          
st         └────────────────────────────────────────────────────────────
218           cases pos_num.cmp a b, exacts [id, congr_arg pos, id] }
id                  └─────────┘            └┘  └───────┘ └─┘  └┘
src           └────┘└─────────┘    └──────┘└┘└┘└───────┘└─┘└┘└┘└┘
typ           └────┘└─────────┘  └──────┘└┘└┘└───────┘└─┘└┘└┘└┘
doc           └────┘               └──────┘  └┘            └┘  └┘
txt           └────┘               └──────┘  └┘            └┘  └┘
par           └────┘               └──────┘  └┘            └┘  └┘
pid                                     └┘  └┘            └┘  
st   ─────────────────────────────┘└───────────────────────────────┘└┘
219  
220    @[simp] theorem lt_to_nat {m n : num} : (m:ℕ) < n ↔ m < n :=
id                                      └─┘             
src                                     └─┘               
typ                                     └─┘             
doc      └──┘                           └─┘
221    show (m:ℕ) < n ↔ cmp m n = ordering.lt, from
id                 └─┘    └─────────┘
src                  └─┘      └─────────┘
typ                └─┘    └─────────┘
222    match cmp m n, cmp_to_nat m n with
id           └─┘    └────────┘  
src          └─┘      └────────┘
typ          └─┘    └────────┘  
223    | ordering.lt, h := by simp at h; simp [h]
id       └─────────┘                           
src      └─────────┘          └───────┘  └────┘ └─
typ      └─────────┘          └───────┘  └────┘└─
doc                           └───────┘  └────┘ └─
txt                           └───────┘  └────┘ └─
par                           └───────┘  └────┘ └─
pid                               └──┘       
st                           └────────────────────
224    | ordering.eq, h := by simp at h; simp [h, lt_irrefl]; exact dec_trivial
id       └─────────┘                             └───────┘
src  ─┘  └─────────┘          └───────┘  └────┘ └┘└───────┘  └────┘           
typ  ─┘  └─────────┘          └───────┘  └────┘└┘└───────┘  └────┘           
doc  ─┘                       └───────┘  └────┘ └┘           └────┘           
txt  ─┘                       └───────┘  └────┘ └┘           └────┘           
par  ─┘                       └───────┘  └────┘ └┘           └────┘           
pid  ─┘                           └──┘       └┘                           
st   ─┘                      └──────────────────────────────────────────────────
225    | ordering.gt, h := by simp [not_lt_of_gt h]; exact dec_trivial
id       └─────────┘                └──────────┘ 
src  ─┘  └─────────┘          └────┘└──────────┘   └────┘           
typ  ─┘  └─────────┘          └────┘└──────────┘  └────┘           
doc  ─┘                       └────┘               └────┘           
txt  ─┘                       └────┘               └────┘           
par  ─┘                       └────┘               └────┘           
pid  ─┘                                                          
st   ─┘                      └─────────────────────────────────────────
226    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
227  
228    @[simp] theorem le_to_nat {m n : num} : (m:ℕ) ≤ n ↔ m ≤ n :=
id                                      └─┘             
src                                     └─┘               
typ                                     └─┘             
doc      └──┘                           └─┘
229    by rw ← not_lt; exact not_congr lt_to_nat
id             └────┘        └───────┘ └───────┘
src       └───┘└────┘  └────┘└───────┘└───────┘
typ       └───┘└────┘  └────┘└───────┘└───────┘
doc       └───┘        └────┘                  
txt       └───┘        └────┘                  
par       └───┘        └────┘                  
pid         └─┘                               
st       └───────────────────────────────────────
230  
src  
typ  
doc  
txt  
par  
pid  
st   
231  end num
232  
233  namespace pos_num
234    @[simp] theorem of_to_nat : Π (n : pos_num), ((n : ℕ) : num) = num.pos n
id                                       └─────┘            └─┘   └─────┘ 
src                                       └─────┘             └─┘   └─────┘
typ                                      └─────┘            └─┘   └─────┘ 
doc      └──┘                             └─────┘              └─┘
235    | 1        := rfl
id                   └─┘
src                  └─┘
typ                  └─┘
236    | (bit0 p) :=
id        └──┘ 
src       └──┘
typ       └──┘ 
237      show ↑(p + p : ℕ) = num.pos p.bit0,
id                       └─────┘  └───┘
src                      └─────┘  └───┘
typ                      └─────┘  └───┘
238      by rw [num.add_of_nat, of_to_nat];
id              └────────────┘  └───────┘
src         └──┘└────────────┘└┘         
typ         └──┘└────────────┘└┘└───────┘
doc         └──┘              └┘         
txt         └──┘              └┘         
par         └──┘              └┘         
pid           └┘              └┘         
st         └─────────────────┘└─────────┘└─
239        exact congr_arg num.pos p.bit0_of_bit0
id               └───────┘ └─────┘ └────────────┘
src        └────┘└───────┘└─────┘└────────────┘
typ        └────┘└───────┘└─────┘└────────────┘
doc        └────┘                              
txt        └────┘                              
par        └────┘                              
pid                                           
st   ─────────────────────────────────────────────
240    | (bit1 p) :=
id        └──┘ 
src  ─┘   └──┘
typ  ─┘   └──┘ 
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
241      show ((p + p : ℕ) : num) + 1 = num.pos p.bit1,
id                         └─┘      └─────┘  └───┘
src                        └─┘      └─────┘  └───┘
typ                        └─┘      └─────┘  └───┘
doc                          └─┘
242      by rw [num.add_of_nat, of_to_nat];
id              └────────────┘  └───────┘
src         └──┘└────────────┘└┘         
typ         └──┘└────────────┘└┘└───────┘
doc         └──┘              └┘         
txt         └──┘              └┘         
par         └──┘              └┘         
pid           └┘              └┘         
st         └─────────────────┘└─────────┘└─
243        exact congr_arg num.pos p.bit1_of_bit1
id               └───────┘ └─────┘ └────────────┘
src        └────┘└───────┘└─────┘└────────────┘
typ        └────┘└───────┘└─────┘└────────────┘
doc        └────┘                              
txt        └────┘                              
par        └────┘                              
pid                                           
st   ────────────────────────────────────────────┘
244  end pos_num
245  
246  namespace num
247  
248    @[simp] theorem of_to_nat : Π (n : num), ((n : ℕ) : num) = n
id                                       └─┘            └─┘   
src                                       └─┘             └─┘  
typ                                      └─┘            └─┘   
doc      └──┘                             └─┘              └─┘
249    | 0           := rfl
id                      └─┘
src                     └─┘
typ                     └─┘
250    | (pos p) := p.of_to_nat
id        └─┘       └────────┘
src       └─┘        └────────┘
typ       └─┘       └────────┘
251  
252    theorem to_nat_inj {m n : num} : (m : ℕ) = n ↔ m = n :=
id                               └─┘               
src                              └─┘                 
typ                              └─┘               
doc                              └─┘
253    ⟨λ h, function.injective_of_left_inverse of_to_nat h, congr_arg _⟩
id          └────────────────────────────────┘ └───────┘   └───────┘
src          └────────────────────────────────┘ └───────┘    └───────┘
typ         └────────────────────────────────┘ └───────┘   └───────┘
254  
255    meta def transfer_rw : tactic unit :=
id                            └────┘ └──┘
src                           └────┘ └──┘
typ                           └────┘ └──┘
doc                                  └──┘
256    `[repeat {rw ← to_nat_inj <|> rw ← lt_to_nat <|> rw ← le_to_nat},
id     └┘
src    └┘└──────┘└───┘          └──┘└───┘         └──┘└───┘         
typ    └┘└──────┘└───┘          └──┘└───┘         └──┘└───┘         
doc      └──────┘└───┘          └──┘└───┘         └──┘└───┘         
txt      └──────┘└───┘          └──┘└───┘         └──┘└───┘         
par      └──────┘└───┘          └──┘└───┘         └──┘└───┘         
pid            └─────┘          └────────┘         └────────┘         
st               └───────────────────────────────────────────────────┘└┘
257      repeat {rw add_to_nat <|> rw mul_to_nat <|> rw cast_one <|> rw cast_zero}]
src      └──────┘└─┘          └──┘└─┘          └──┘└─┘        └──┘└─┘         
typ      └──────┘└─┘          └──┘└─┘          └──┘└─┘        └──┘└─┘         
doc      └──────┘└─┘          └──┘└─┘          └──┘└─┘        └──┘└─┘         
txt      └──────┘└─┘          └──┘└─┘          └──┘└─┘        └──┘└─┘         
par      └──────┘└─┘          └──┘└─┘          └──┘└─┘        └──┘└─┘         
pid            └───┘          └──────┘          └──────┘        └──────┘         
st               └─────────────────────────────────────┘└──────┘└──────┘└───────┘└┘
258  
259    meta def transfer : tactic unit := `[intros, transfer_rw, try {simp}]
id                         └────┘ └──┘    └┘        └─────────┘
src                        └────┘ └──┘    └┘└────┘  └─────────┘  └───┘└──┘
typ                        └────┘ └──┘    └┘└────┘  └─────────┘  └───┘└──┘
doc                               └──┘      └────┘               └───┘└──┘
txt                                         └────┘               └───┘└──┘
par                                         └────┘  └─────────┘  └───┘└──┘
pid                                                                 └─────┘
st                                                  └─────────┘       └────┘
260  
261    instance : comm_semiring num :=
id                └───────────┘ └─┘
src               └───────────┘ └─┘
typ               └───────────┘ └─┘
doc                             └─┘
262    by refine {
src       └─────┘ 
typ       └─────┘ 
doc       └─────┘ 
txt       └─────┘ 
par       └─────┘ 
pid              
st       └─────────
263      add      := (+),
id                   
src  ───────────────┘└───
typ  ───────────────┘└───
doc  ───────────────┘ └───
txt  ───────────────┘ └───
par  ───────────────┘ └───
pid  ───────────────┘ └───
st   ─────────────────────
264      zero     := 0,
src  ───────────────────
typ  ───────────────────
doc  ───────────────────
txt  ───────────────────
par  ───────────────────
pid  ───────────────────
st   ───────────────────
265      zero_add := zero_add,
id                   └──────┘
src  ───────────────┘└──────┘└─
typ  ───────────────┘└──────┘└─
doc  ───────────────┘        └─
txt  ───────────────┘        └─
par  ───────────────┘        └─
pid  ───────────────┘        └─
st   ──────────────────────────
266      add_zero := add_zero,
id                   └──────┘
src  ───────────────┘└──────┘└─
typ  ───────────────┘└──────┘└─
doc  ───────────────┘        └─
txt  ───────────────┘        └─
par  ───────────────┘        └─
pid  ───────────────┘        └─
st   ──────────────────────────
267      mul      := (*),
id                   
src  ───────────────┘└───
typ  ───────────────┘└───
doc  ───────────────┘ └───
txt  ───────────────┘ └───
par  ───────────────┘ └───
pid  ───────────────┘ └───
st   ─────────────────────
268      one      := 1, .. }; try {transfer}; simp [mul_add, mul_left_comm, mul_comm]
id                                 └──────┘         └─────┘  └───────────┘  └──────┘
src  ──────────────────────┘  └───┘└──────┘  └────┘└─────┘└┘└───────────┘└┘└──────┘└─
typ  ──────────────────────┘  └───┘└──────┘  └────┘└─────┘└┘└───────────┘└┘└──────┘└─
doc  ──────────────────────┘  └───┘          └────┘       └┘             └┘        └─
txt  ──────────────────────┘  └───┘          └────┘       └┘             └┘        └─
par  ──────────────────────┘  └───┘└──────┘  └────┘       └┘             └┘        └─
pid  ──────────────────────┘     └┘                     └┘             └┘        
st   ─────────────────────────────┘└──────┘└┘└────────────────────────────────────────
269  
src  
typ  
doc  
txt  
par  
pid  
st   
270    instance : ordered_cancel_comm_monoid num :=
id                └────────────────────────┘ └─┘
src  ─┘           └────────────────────────┘ └─┘
typ  ─┘           └────────────────────────┘ └─┘
doc  ─┘                                      └─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
271    { add_left_cancel            := by {intros a b c, transfer_rw, apply add_left_cancel},
id                                                       └─────────┘        └─────────────┘
src                                        └──────────┘  └─────────┘  └────┘└─────────────┘
typ                                        └──────────┘  └─────────┘  └────┘└─────────────┘
doc                                        └──────────┘               └────┘
txt                                        └──────────┘               └────┘
par                                        └──────────┘  └─────────┘  └────┘
pid                                              └────┘                    
st                                       └────────────┘└───────────┘└─────────────────────┘└┘
272      add_right_cancel           := by {intros a b c, transfer_rw, apply add_right_cancel},
id                                                       └─────────┘        └──────────────┘
src                                        └──────────┘  └─────────┘  └────┘└──────────────┘
typ                                        └──────────┘  └─────────┘  └────┘└──────────────┘
doc                                        └──────────┘               └────┘
txt                                        └──────────┘               └────┘
par                                        └──────────┘  └─────────┘  └────┘
pid                                              └────┘                    
st                                       └────────────┘└───────────┘└──────────────────────┘└┘
273      lt                         := (<),
id                                     
src                                    
typ                                    
274      lt_iff_le_not_le           := by {intros a b, transfer_rw, apply lt_iff_le_not_le},
id                                                     └─────────┘        └──────────────┘
src                                        └────────┘  └─────────┘  └────┘└──────────────┘
typ                                        └────────┘  └─────────┘  └────┘└──────────────┘
doc                                        └────────┘               └────┘
txt                                        └────────┘               └────┘
par                                        └────────┘  └─────────┘  └────┘
pid                                              └──┘                    
st                                       └──────────┘└───────────┘└──────────────────────┘└┘
275      le                         := (≤),
id                                     
src                                    
typ                                    
276      le_refl                    := by transfer,
id                                        └──────┘
src                                       └──────┘
typ                                       └──────┘
par                                       └──────┘
st                                       └───────┘
277      le_trans                   := by {intros a b c, transfer_rw, apply le_trans},
id                                                       └─────────┘        └──────┘
src                                        └──────────┘  └─────────┘  └────┘└──────┘
typ                                        └──────────┘  └─────────┘  └────┘└──────┘
doc                                        └──────────┘               └────┘
txt                                        └──────────┘               └────┘
par                                        └──────────┘  └─────────┘  └────┘
pid                                              └────┘                    
st                                       └────────────┘└───────────┘└──────────────┘└┘
278      le_antisymm                := by {intros a b, transfer_rw, apply le_antisymm},
id                                                     └─────────┘        └─────────┘
src                                        └────────┘  └─────────┘  └────┘└─────────┘
typ                                        └────────┘  └─────────┘  └────┘└─────────┘
doc                                        └────────┘               └────┘
txt                                        └────────┘               └────┘
par                                        └────────┘  └─────────┘  └────┘
pid                                              └──┘                    
st                                       └──────────┘└───────────┘└─────────────────┘└┘
279      add_le_add_left            := by {intros a b h c, revert h, transfer_rw, exact λ h, add_le_add_left h c},
id                                                                   └─────────┘             └─────────────┘   
src                                        └────────────┘  └──────┘  └─────────┘  └────┘ └──┘└─────────────┘ 
typ                                        └────────────┘  └──────┘  └─────────┘  └────┘ └──┘└─────────────┘ 
doc                                        └────────────┘  └──────┘               └────┘ └──┘                
txt                                        └────────────┘  └──────┘               └────┘ └──┘                
par                                        └────────────┘  └──────┘  └─────────┘  └────┘ └──┘                
pid                                              └──────┘        └┘                     └──┘                
st                                       └──────────────┘└────────┘└───────────┘└──────────────────────────────┘└┘
280      le_of_add_le_add_left      := by {intros a b c, transfer_rw, apply le_of_add_le_add_left},
id                                                       └─────────┘        └───────────────────┘
src                                        └──────────┘  └─────────┘  └────┘└───────────────────┘
typ                                        └──────────┘  └─────────┘  └────┘└───────────────────┘
doc                                        └──────────┘               └────┘
txt                                        └──────────┘               └────┘
par                                        └──────────┘  └─────────┘  └────┘
pid                                              └────┘                    
st                                       └────────────┘└───────────┘└───────────────────────────┘└┘
281      ..num.comm_semiring }
id         └───────────────┘
src        └───────────────┘
typ        └───────────────┘
282  
283    instance : decidable_linear_ordered_semiring num :=
id                └───────────────────────────────┘ └─┘
src               └───────────────────────────────┘ └─┘
typ               └───────────────────────────────┘ └─┘
doc                                                 └─┘
284    { le_total                   := by {intros a b, transfer_rw, apply le_total},
id                                                     └─────────┘        └──────┘
src                                        └────────┘  └─────────┘  └────┘└──────┘
typ                                        └────────┘  └─────────┘  └────┘└──────┘
doc                                        └────────┘               └────┘
txt                                        └────────┘               └────┘
par                                        └────────┘  └─────────┘  └────┘
pid                                              └──┘                    
st                                       └──────────┘└───────────┘└──────────────┘└┘
285      zero_lt_one                := dec_trivial,
id                                     └─────────┘
src                                    └─────────┘
typ                                    └─────────┘
doc                                    └─────────┘
286      mul_le_mul_of_nonneg_left  := by {intros a b c, transfer_rw, apply mul_le_mul_of_nonneg_left},
id                                                       └─────────┘        └───────────────────────┘
src                                        └──────────┘  └─────────┘  └────┘└───────────────────────┘
typ                                        └──────────┘  └─────────┘  └────┘└───────────────────────┘
doc                                        └──────────┘               └────┘
txt                                        └──────────┘               └────┘
par                                        └──────────┘  └─────────┘  └────┘
pid                                              └────┘                    
st                                       └────────────┘└───────────┘└───────────────────────────────┘└┘
287      mul_le_mul_of_nonneg_right := by {intros a b c, transfer_rw, apply mul_le_mul_of_nonneg_right},
id                                                       └─────────┘        └────────────────────────┘
src                                        └──────────┘  └─────────┘  └────┘└────────────────────────┘
typ                                        └──────────┘  └─────────┘  └────┘└────────────────────────┘
doc                                        └──────────┘               └────┘
txt                                        └──────────┘               └────┘
par                                        └──────────┘  └─────────┘  └────┘
pid                                              └────┘                    
st                                       └────────────┘└───────────┘└────────────────────────────────┘└┘
288      mul_lt_mul_of_pos_left     := by {intros a b c, transfer_rw, apply mul_lt_mul_of_pos_left},
id                                                       └─────────┘        └────────────────────┘
src                                        └──────────┘  └─────────┘  └────┘└────────────────────┘
typ                                        └──────────┘  └─────────┘  └────┘└────────────────────┘
doc                                        └──────────┘               └────┘
txt                                        └──────────┘               └────┘
par                                        └──────────┘  └─────────┘  └────┘
pid                                              └────┘                    
st                                       └────────────┘└───────────┘└────────────────────────────┘└┘
289      mul_lt_mul_of_pos_right    := by {intros a b c, transfer_rw, apply mul_lt_mul_of_pos_right},
id                                                       └─────────┘        └─────────────────────┘
src                                        └──────────┘  └─────────┘  └────┘└─────────────────────┘
typ                                        └──────────┘  └─────────┘  └────┘└─────────────────────┘
doc                                        └──────────┘               └────┘
txt                                        └──────────┘               └────┘
par                                        └──────────┘  └─────────┘  └────┘
pid                                              └────┘                    
st                                       └────────────┘└───────────┘└─────────────────────────────┘└┘
290      decidable_lt               := num.decidable_lt,
id                                     └──────────────┘
src                                    └──────────────┘
typ                                    └──────────────┘
291      decidable_le               := num.decidable_le,
id                                     └──────────────┘
src                                    └──────────────┘
typ                                    └──────────────┘
292      decidable_eq               := num.decidable_eq,
id                                     └──────────────┘
src                                    └──────────────┘
typ                                    └──────────────┘
293      ..num.comm_semiring, ..num.ordered_cancel_comm_monoid }
id         └───────────────┘    └────────────────────────────┘
src        └───────────────┘    └────────────────────────────┘
typ        └───────────────┘    └────────────────────────────┘
294  
295    @[simp] theorem dvd_to_nat (m n : num) : (m : ℕ) ∣ n ↔ m ∣ n :=
id                                       └─┘               
src                                      └─┘                 
typ                                      └─┘               
doc      └──┘                            └─┘
296    ⟨λ ⟨k, e⟩, ⟨k, by rw [← of_to_nat n, e]; simp⟩,
id                           └───────┘   
src                      └────┘└───────┘ └┘   └──┘
typ                    └────┘└───────┘└┘  └──┘
doc                      └────┘          └┘   └──┘
txt                      └────┘          └┘   └──┘
par                      └────┘          └┘   └──┘
pid                        └──┘          └┘ 
st                      └────────────────┘└─┘└────┘
297     λ ⟨k, e⟩, ⟨k, by simp [e]⟩⟩
id                           
src                      └────┘ 
typ                    └────┘
doc                      └────┘ 
txt                      └────┘ 
par                      └────┘ 
pid                           
st                      └───────┘
298  
299  end num
300  
301  namespace pos_num
302    variables {α : Type*}
303    open num
304  
305    theorem to_nat_inj {m n : pos_num} : (m : ℕ) = n ↔ m = n :=
id                               └─────┘               
src                              └─────┘                 
typ                              └─────┘               
doc                              └─────┘
306    ⟨λ h, num.pos.inj $ by rw [← pos_num.of_to_nat, ← pos_num.of_to_nat, h],
id          └─────────┘            └───────────────┘    └───────────────┘  
src          └─────────┘      └────┘└───────────────┘└──┘└───────────────┘└┘ 
typ         └─────────┘      └────┘└───────────────┘└──┘└───────────────┘└┘
doc                           └────┘                 └──┘                 └┘ 
txt                           └────┘                 └──┘                 └┘ 
par                           └────┘                 └──┘                 └┘ 
pid                             └──┘                 └──┘                 └┘ 
st                           └──────────────────────┘└───────────────────┘└─┘
307     congr_arg _⟩
id      └───────┘
src     └───────┘
typ     └───────┘
308  
309    theorem pred'_to_nat : ∀ n, (pred' n : ℕ) = nat.pred n
id                                 └───┘       └──────┘ 
src                                 └───┘        └──────┘
typ                                └───┘       └──────┘ 
310    | 1        := rfl
id                   └─┘
src                  └─┘
typ                  └─┘
311    | (bit0 n) :=
id        └──┘ 
src       └──┘
typ       └──┘ 
312      have nat.succ ↑(pred' n) = ↑n,
id            └──────┘  └───┘     
src           └──────┘  └───┘     
typ           └──────┘  └───┘     
313      by rw [pred'_to_nat n, nat.succ_pred_eq_of_pos (to_nat_pos n)],
id              └──────────┘   └─────────────────────┘  └────────┘ 
src         └──┘             └┘└─────────────────────┘ └────────┘ └┘
typ         └──┘└──────────┘└┘└─────────────────────┘ └────────┘└┘
doc         └──┘             └┘                                   └┘
txt         └──┘             └┘                                   └┘
par         └──┘             └┘                                   └┘
pid           └┘             └┘                                   └┘
st         └─────────────────┘└──────────────────────────────────────┘
314      match pred' n, this : ∀ k : num, nat.succ ↑k = ↑n →
id             └───┘    └──┘         └─┘  └──────┘   
src            └───┘                 └─┘  └──────┘    
typ            └───┘    └──┘         └─┘  └──────┘   
doc                                  └─┘
315        ↑(num.cases_on k 1 bit1 : pos_num) = nat.pred (_root_.bit0 n) with
id          └──────────┘    └──┘   └─────┘   └──────┘  └─────────┘
src         └──────────┘     └──┘   └─────┘   └──────┘  └─────────┘
typ         └──────────┘    └──┘   └─────┘   └──────┘  └─────────┘
doc                                  └─────┘
316      | 0, (h : ((1:num):ℕ) = n) := by rw ← to_nat_inj.1 h; refl
id                     └─┘                   └────────┘   
src                    └─┘              └───┘└────────┘└─┘   └────
typ                    └─┘              └───┘└────────┘└─┘  └────
doc                    └─┘                └───┘          └─┘   └────
txt                                       └───┘          └─┘   └────
par                                       └───┘          └─┘   └────
pid                                         └─┘          └─┘       
st                                       └──────────────────────────
317      | num.pos p, (h : nat.succ ↑p = n) :=
id         └─────┘         └──────┘   
src  ───┘  └─────┘         └──────┘   
typ  ───┘  └─────┘         └──────┘   
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘
318        by rw ← h; exact (nat.succ_add p p).symm
id                          └──────────┘   
src           └───┘   └────┘ └──────────┘  └──────
typ           └───┘  └────┘ └──────────┘ └──────
doc           └───┘   └────┘               └──────
txt           └───┘   └────┘               └──────
par           └───┘   └────┘               └──────
pid             └─┘                       └───┘└─
st           └──────────────────────────────────────
319      end
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘
320    | (bit1 n) := rfl
id        └──┘       └─┘
src       └──┘       └─┘
typ       └──┘       └─┘
321  
322    @[simp] theorem pred'_succ' (n) : pred' (succ' n) = n :=
id                                       └───┘  └───┘    
src                                      └───┘  └───┘    
typ                                      └───┘  └───┘    
doc      └──┘
323    num.to_nat_inj.1 $ by rw [pred'_to_nat, succ'_to_nat,
id     └────────────┘           └──────────┘  └──────────┘
src    └────────────┘       └──┘└──────────┘└┘└──────────┘└─
typ    └────────────┘       └──┘└──────────┘└┘└──────────┘└─
doc                          └──┘            └┘            └─
txt                          └──┘            └┘            └─
par                          └──┘            └┘            └─
pid                            └┘            └┘            └─
st                          └───────────────┘└────────────┘└─
324      nat.add_one, nat.pred_succ]
id       └─────────┘  └───────────┘
src  ───┘└─────────┘└┘└───────────┘└─
typ  ───┘└─────────┘└┘└───────────┘└─
doc  ───┘           └┘             └─
txt  ───┘           └┘             └─
par  ───┘           └┘             └─
pid  ───┘           └┘             
st   ──────────────┘└─────────────┘
325  
src  
typ  
doc  
txt  
par  
pid  
st   
326    @[simp] theorem succ'_pred' (n) : succ' (pred' n) = n :=
id                                       └───┘  └───┘    
src  ─┘                                  └───┘  └───┘    
typ  ─┘                                  └───┘  └───┘    
doc  ─┘  └──┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
327    to_nat_inj.1 $ by rw [succ'_to_nat, pred'_to_nat,
id     └────────┘           └──────────┘  └──────────┘
src    └────────┘       └──┘└──────────┘└┘└──────────┘└─
typ    └────────┘       └──┘└──────────┘└┘└──────────┘└─
doc                      └──┘            └┘            └─
txt                      └──┘            └┘            └─
par                      └──┘            └┘            └─
pid                        └┘            └┘            └─
st                      └───────────────┘└────────────┘└─
328      nat.add_one, nat.succ_pred_eq_of_pos (to_nat_pos _)]
id       └─────────┘  └─────────────────────┘  └────────┘
src  ───┘└─────────┘└┘└─────────────────────┘ └────────┘└────
typ  ───┘└─────────┘└┘└─────────────────────┘ └────────┘└────
doc  ───┘           └┘                                  └────
txt  ───┘           └┘                                  └────
par  ───┘           └┘                                  └────
pid  ───┘           └┘                                  └──┘
st   ──────────────┘└──────────────────────────────────────┘
329  
src  
typ  
doc  
txt  
par  
pid  
st   
330    theorem size_to_nat : ∀ n, (size n : ℕ) = nat.size n
id                                └──┘       └──────┘ 
src  ─┘                            └──┘        └──────┘
typ  ─┘                           └──┘       └──────┘ 
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
331    | 1        := nat.size_one.symm
id                   └──────────┘└───┘
src                  └──────────┘└───┘
typ                  └──────────┘└───┘
332    | (bit0 n) := by rw [size, succ_to_nat, size_to_nat, cast_bit0,
id        └──┘              └──┘  └─────────┘  └─────────┘  └───────┘
src       └──┘          └──┘└──┘└┘└─────────┘└┘           └┘└───────┘└─
typ       └──┘          └──┘└──┘└┘└─────────┘└┘└─────────┘└┘└───────┘└─
doc                     └──┘    └┘           └┘           └┘         └─
txt                     └──┘    └┘           └┘           └┘         └─
par                     └──┘    └┘           └┘           └┘         └─
pid                       └┘    └┘           └┘           └┘         └─
st                     └───────┘└───────────┘└───────────┘└─────────┘└─
333                         nat.size_bit0 $ ne_of_gt $ to_nat_pos n]
id                          └───────────┘   └──────┘   └────────┘ 
src  ──────────────────────┘└───────────┘ └──────┘ └────────┘ └─
typ  ──────────────────────┘└───────────┘ └──────┘ └────────┘└─
doc  ──────────────────────┘                                  └─
txt  ──────────────────────┘                                  └─
par  ──────────────────────┘                                  └─
pid  ──────────────────────┘                                  
st   ─────────────────────────────────────────────────────────────┘
334    | (bit1 n) := by rw [size, succ_to_nat, size_to_nat, cast_bit1,
id        └──┘              └──┘  └─────────┘  └─────────┘  └───────┘
src  ─┘   └──┘          └──┘└──┘└┘└─────────┘└┘           └┘└───────┘└─
typ  ─┘   └──┘          └──┘└──┘└┘└─────────┘└┘└─────────┘└┘└───────┘└─
doc  ─┘                 └──┘    └┘           └┘           └┘         └─
txt  ─┘                 └──┘    └┘           └┘           └┘         └─
par  ─┘                 └──┘    └┘           └┘           └┘         └─
pid  ─┘                   └┘    └┘           └┘           └┘         └─
st   ─┘                └───────┘└───────────┘└───────────┘└─────────┘└─
335                         nat.size_bit1]
id                          └───────────┘
src  ──────────────────────┘└───────────┘└─
typ  ──────────────────────┘└───────────┘└─
doc  ──────────────────────┘             └─
txt  ──────────────────────┘             └─
par  ──────────────────────┘             └─
pid  ──────────────────────┘             
st   ───────────────────────────────────┘
336  
src  
typ  
doc  
txt  
par  
pid  
st   
337    theorem size_eq_nat_size : ∀ n, (size n : ℕ) = nat_size n
id                                     └──┘       └──────┘ 
src  ─┘                                 └──┘        └──────┘
typ  ─┘                                └──┘       └──────┘ 
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
338    | 1        := rfl
id                   └─┘
src                  └─┘
typ                  └─┘
339    | (bit0 n) := by rw [size, succ_to_nat, nat_size, size_eq_nat_size]
id        └──┘              └──┘  └─────────┘  └──────┘  └──────────────┘
src       └──┘          └──┘└──┘└┘└─────────┘└┘└──────┘└┘                └─
typ       └──┘          └──┘└──┘└┘└─────────┘└┘└──────┘└┘└──────────────┘└─
doc                     └──┘    └┘           └┘        └┘                └─
txt                     └──┘    └┘           └┘        └┘                └─
par                     └──┘    └┘           └┘        └┘                └─
pid                       └┘    └┘           └┘        └┘                
st                     └───────┘└───────────┘└────────┘└────────────────┘
340    | (bit1 n) := by rw [size, succ_to_nat, nat_size, size_eq_nat_size]
id        └──┘              └──┘  └─────────┘  └──────┘  └──────────────┘
src  ─┘   └──┘          └──┘└──┘└┘└─────────┘└┘└──────┘└┘                └─
typ  ─┘   └──┘          └──┘└──┘└┘└─────────┘└┘└──────┘└┘└──────────────┘└─
doc  ─┘                 └──┘    └┘           └┘        └┘                └─
txt  ─┘                 └──┘    └┘           └┘        └┘                └─
par  ─┘                 └──┘    └┘           └┘        └┘                └─
pid  ─┘                   └┘    └┘           └┘        └┘                
st   ─┘                └───────┘└───────────┘└────────┘└────────────────┘
341  
src  
typ  
doc  
txt  
par  
pid  
st   
342    theorem nat_size_to_nat (n) : nat_size n = nat.size n :=
id                                   └──────┘   └──────┘ 
src  ─┘                              └──────┘    └──────┘
typ  ─┘                              └──────┘   └──────┘ 
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
343    by rw [← size_eq_nat_size, size_to_nat]
id              └──────────────┘  └─────────┘
src       └────┘└──────────────┘└┘└─────────┘└─
typ       └────┘└──────────────┘└┘└─────────┘└─
doc       └────┘                └┘           └─
txt       └────┘                └┘           └─
par       └────┘                └┘           └─
pid         └──┘                └┘           
st       └─────────────────────┘└───────────┘
344  
src  
typ  
doc  
txt  
par  
pid  
st   
345    theorem nat_size_pos (n) : 0 < nat_size n :=
id                                   └──────┘ 
src  ─┘                              └──────┘
typ  ─┘                              └──────┘ 
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
346    by cases n; apply nat.succ_pos
id                      └──────────┘
src       └────┘   └────┘└──────────┘
typ       └────┘  └────┘└──────────┘
doc       └────┘   └────┘            
txt       └────┘   └────┘            
par       └────┘   └────┘            
pid                                
st       └────────────────────────────
347  
src  
typ  
doc  
txt  
par  
pid  
st   
348    meta def transfer_rw : tactic unit :=
id                            └────┘ └──┘
src  ─┘                       └────┘ └──┘
typ  ─┘                       └────┘ └──┘
doc  ─┘                              └──┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
349    `[repeat {rw ← to_nat_inj <|> rw ← lt_to_nat <|> rw ← le_to_nat},
id     └┘
src    └┘└──────┘└───┘          └──┘└───┘         └──┘└───┘         
typ    └┘└──────┘└───┘          └──┘└───┘         └──┘└───┘         
doc      └──────┘└───┘          └──┘└───┘         └──┘└───┘         
txt      └──────┘└───┘          └──┘└───┘         └──┘└───┘         
par      └──────┘└───┘          └──┘└───┘         └──┘└───┘         
pid            └─────┘          └────────┘         └────────┘         
st               └───────────────────────────────────────────────────┘└┘
350      repeat {rw add_to_nat <|> rw mul_to_nat <|> rw cast_one <|> rw cast_zero}]
src      └──────┘└─┘          └──┘└─┘          └──┘└─┘        └──┘└─┘         
typ      └──────┘└─┘          └──┘└─┘          └──┘└─┘        └──┘└─┘         
doc      └──────┘└─┘          └──┘└─┘          └──┘└─┘        └──┘└─┘         
txt      └──────┘└─┘          └──┘└─┘          └──┘└─┘        └──┘└─┘         
par      └──────┘└─┘          └──┘└─┘          └──┘└─┘        └──┘└─┘         
pid            └───┘          └──────┘          └──────┘        └──────┘         
st               └──────────────────────────────────────────────────────────────┘└┘
351  
352    meta def transfer : tactic unit := `[intros, transfer_rw, try {simp [mul_comm, mul_left_comm]}]
id                         └────┘ └──┘    └┘        └─────────┘
src                        └────┘ └──┘    └┘└────┘  └─────────┘  └───┘└────┘        └┘             
typ                        └────┘ └──┘    └┘└────┘  └─────────┘  └───┘└────┘        └┘             
doc                               └──┘      └────┘               └───┘└────┘        └┘             
txt                                         └────┘               └───┘└────┘        └┘             
par                                         └────┘  └─────────┘  └───┘└────┘        └┘             
pid                                                                 └──────┘        └┘             └┘
st                                                  └─────────┘       └────────────────────────────┘└┘
353  
354    instance : add_comm_semigroup pos_num :=
id                └────────────────┘ └─────┘
src               └────────────────┘ └─────┘
typ               └────────────────┘ └─────┘
doc                                  └─────┘
355    by refine {add := (+), ..}; transfer
id                                └──────┘
src       └─────┘ └─────┘└─────┘  └──────┘
typ       └─────┘ └─────┘└─────┘  └──────┘
doc       └─────┘ └─────┘ └─────┘
txt       └─────┘ └─────┘ └─────┘
par       └─────┘ └─────┘ └─────┘  └──────┘
pid              └─────┘ └─────┘
st       └────────────────────────────────┘
356  
357    instance : comm_monoid pos_num :=
id                └─────────┘ └─────┘
src               └─────────┘ └─────┘
typ               └─────────┘ └─────┘
doc                           └─────┘
358    by refine {mul := (*), one := 1, ..}; transfer
id                                          └──────┘
src       └─────┘ └─────┘└───────────────┘  └──────┘
typ       └─────┘ └─────┘└───────────────┘  └──────┘
doc       └─────┘ └─────┘ └───────────────┘
txt       └─────┘ └─────┘ └───────────────┘
par       └─────┘ └─────┘ └───────────────┘  └──────┘
pid              └─────┘ └───────────────┘
st       └──────────────────────────────────────────┘
359  
360  
361    instance : distrib pos_num :=
id                └─────┘ └─────┘
src               └─────┘ └─────┘
typ               └─────┘ └─────┘
doc                       └─────┘
362    by refine {add := (+), mul := (*), ..}; {transfer, simp [mul_add, mul_comm]}
id                                            └──────┘        └─────┘  └──────┘
src       └─────┘ └─────┘└─────────┘└─────┘   └──────┘  └────┘└─────┘└┘└──────┘
typ       └─────┘ └─────┘└─────────┘└─────┘   └──────┘  └────┘└─────┘└┘└──────┘
doc       └─────┘ └─────┘ └─────────┘ └─────┘             └────┘       └┘        
txt       └─────┘ └─────┘ └─────────┘ └─────┘             └────┘       └┘        
par       └─────┘ └─────┘ └─────────┘ └─────┘   └──────┘  └────┘       └┘        
pid              └─────┘ └─────────┘ └─────┘                        └┘        
st       └────────────────────────────────────┘└───────┘└────────────────────────┘└┘
363  
364    instance : decidable_linear_order pos_num :=
id                └────────────────────┘ └─────┘
src               └────────────────────┘ └─────┘
typ               └────────────────────┘ └─────┘
doc                                      └─────┘
365    { lt              := (<),
id                          
src                         
typ                         
366      lt_iff_le_not_le := by {intros a b, transfer_rw, apply lt_iff_le_not_le},
id                                           └─────────┘        └──────────────┘
src                              └────────┘  └─────────┘  └────┘└──────────────┘
typ                              └────────┘  └─────────┘  └────┘└──────────────┘
doc                              └────────┘               └────┘
txt                              └────────┘               └────┘
par                              └────────┘  └─────────┘  └────┘
pid                                    └──┘                    
st                             └──────────┘└───────────┘└──────────────────────┘└┘
367      le              := (≤),
id                          
src                         
typ                         
368      le_refl         := by transfer,
id                             └──────┘
src                            └──────┘
typ                            └──────┘
par                            └──────┘
st                            └───────┘
369      le_trans        := by {intros a b c, transfer_rw, apply le_trans},
id                                            └─────────┘        └──────┘
src                             └──────────┘  └─────────┘  └────┘└──────┘
typ                             └──────────┘  └─────────┘  └────┘└──────┘
doc                             └──────────┘               └────┘
txt                             └──────────┘               └────┘
par                             └──────────┘  └─────────┘  └────┘
pid                                   └────┘                    
st                            └────────────┘└───────────┘└──────────────┘└┘
370      le_antisymm     := by {intros a b, transfer_rw, apply le_antisymm},
id                                          └─────────┘        └─────────┘
src                             └────────┘  └─────────┘  └────┘└─────────┘
typ                             └────────┘  └─────────┘  └────┘└─────────┘
doc                             └────────┘               └────┘
txt                             └────────┘               └────┘
par                             └────────┘  └─────────┘  └────┘
pid                                   └──┘                    
st                            └──────────┘└───────────┘└─────────────────┘└┘
371      le_total        := by {intros a b, transfer_rw, apply le_total},
id                                          └─────────┘        └──────┘
src                             └────────┘  └─────────┘  └────┘└──────┘
typ                             └────────┘  └─────────┘  └────┘└──────┘
doc                             └────────┘               └────┘
txt                             └────────┘               └────┘
par                             └────────┘  └─────────┘  └────┘
pid                                   └──┘                    
st                            └──────────┘└───────────┘└──────────────┘└┘
372      decidable_lt    := by apply_instance,
src                            └────────────┘
typ                            └────────────┘
doc                            └────────────┘
txt                            └────────────┘
par                            └────────────┘
st                            └─────────────┘
373      decidable_le    := by apply_instance,
src                            └────────────┘
typ                            └────────────┘
doc                            └────────────┘
txt                            └────────────┘
par                            └────────────┘
st                            └─────────────┘
374      decidable_eq    := by apply_instance }
src                            └─────────────┘
typ                            └─────────────┘
doc                            └─────────────┘
txt                            └─────────────┘
par                            └─────────────┘
pid                                          
st                            └──────────────┘
375  
376    @[simp] theorem cast_to_num (n : pos_num) : ↑n = num.pos n :=
id                                      └─────┘      └─────┘ 
src                                     └─────┘       └─────┘
typ                                     └─────┘      └─────┘ 
doc      └──┘                           └─────┘
377    by rw [← cast_to_nat, ← of_to_nat n]
id              └─────────┘    └───────┘ 
src       └────┘└─────────┘└──┘└───────┘ └─
typ       └────┘└─────────┘└──┘└───────┘└─
doc       └────┘           └──┘          └─
txt       └────┘           └──┘          └─
par       └────┘           └──┘          └─
pid         └──┘           └──┘          
st       └────────────────┘└─────────────┘
378  
src  
typ  
doc  
txt  
par  
pid  
st   
379    theorem bit_to_nat (b n) : (bit b n : ℕ) = nat.bit b n :=
id                                 └─┘        └─────┘  
src  ─┘                            └─┘          └─────┘
typ  ─┘                            └─┘        └─────┘  
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
380    by cases b; refl
id              
src       └────┘   └────
typ       └────┘  └────
doc       └────┘   └────
txt       └────┘   └────
par       └────┘   └────
pid                   
st       └──────────────
381  
src  
typ  
doc  
txt  
par  
pid  
st   
382    @[simp] theorem cast_add [add_monoid α] [has_one α] (m n) : ((m + n : pos_num) : α) = m + n :=
id                               └────────┘    └─────┘                  └─────┘         
src  ─┘                          └────────┘     └─────┘                     └─────┘          
typ  ─┘                          └────────┘    └─────┘                  └─────┘         
doc  ─┘  └──┘                                                                └─────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
383    by rw [← cast_to_nat, add_to_nat, nat.cast_add, cast_to_nat, cast_to_nat]
id              └─────────┘  └────────┘  └──────────┘  └─────────┘  └─────────┘
src       └────┘└─────────┘└┘└────────┘└┘└──────────┘└┘└─────────┘└┘└─────────┘└─
typ       └────┘└─────────┘└┘└────────┘└┘└──────────┘└┘└─────────┘└┘└─────────┘└─
doc       └────┘           └┘          └┘            └┘           └┘           └─
txt       └────┘           └┘          └┘            └┘           └┘           └─
par       └────┘           └┘          └┘            └┘           └┘           └─
pid         └──┘           └┘          └┘            └┘           └┘           
st       └────────────────┘└──────────┘└────────────┘└───────────┘└───────────┘
384  
src  
typ  
doc  
txt  
par  
pid  
st   
385    @[simp] theorem cast_succ [add_monoid α] [has_one α] (n : pos_num) : (succ n : α) = n + 1 :=
id                                └────────┘    └─────┘        └─────┘     └──┘        
src  ─┘                           └────────┘     └─────┘         └─────┘     └──┘           
typ  ─┘                           └────────┘    └─────┘        └─────┘     └──┘        
doc  ─┘  └──┘                                                    └─────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
386    by rw [← add_one, cast_add, cast_one]
id              └─────┘  └──────┘  └──────┘
src       └────┘└─────┘└┘└──────┘└┘└──────┘└─
typ       └────┘└─────┘└┘└──────┘└┘└──────┘└─
doc       └────┘       └┘        └┘        └─
txt       └────┘       └┘        └┘        └─
par       └────┘       └┘        └┘        └─
pid         └──┘       └┘        └┘        
st       └────────────┘└────────┘└────────┘
387  
src  
typ  
doc  
txt  
par  
pid  
st   
388    @[simp] theorem cast_inj [add_monoid α] [has_one α] [char_zero α] {m n : pos_num} : (m:α) = n ↔ m = n :=
id                               └────────┘    └─────┘    └───────┘          └─────┘             
src  ─┘                          └────────┘     └─────┘     └───────┘           └─────┘                
typ  ─┘                          └────────┘    └─────┘    └───────┘          └─────┘             
doc  ─┘  └──┘                                               └───────┘           └─────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
389    by rw [← cast_to_nat m, ← cast_to_nat n, nat.cast_inj, to_nat_inj]
id              └─────────┘     └─────────┘   └──────────┘  └────────┘
src       └────┘└─────────┘ └──┘└─────────┘ └┘└──────────┘└┘└────────┘└─
typ       └────┘└─────────┘└──┘└─────────┘└┘└──────────┘└┘└────────┘└─
doc       └────┘            └──┘            └┘            └┘          └─
txt       └────┘            └──┘            └┘            └┘          └─
par       └────┘            └──┘            └┘            └┘          └─
pid         └──┘            └──┘            └┘            └┘          
st       └──────────────────┘└───────────────┘└────────────┘└──────────┘
390  
src  
typ  
doc  
txt  
par  
pid  
st   
391    theorem one_le_cast [linear_ordered_semiring α] (n : pos_num) : (1 : α) ≤ n :=
id                          └─────────────────────┘        └─────┘            
src  ─┘                     └─────────────────────┘         └─────┘            
typ  ─┘                     └─────────────────────┘        └─────┘            
doc  ─┘                                                     └─────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
392    by rw [← cast_to_nat, ← nat.cast_one, nat.cast_le]; apply to_nat_pos
id              └─────────┘    └──────────┘  └─────────┘         └────────┘
src       └────┘└─────────┘└──┘└──────────┘└┘└─────────┘  └────┘└────────┘
typ       └────┘└─────────┘└──┘└──────────┘└┘└─────────┘  └────┘└────────┘
doc       └────┘           └──┘            └┘             └────┘          
txt       └────┘           └──┘            └┘             └────┘          
par       └────┘           └──┘            └┘             └────┘          
pid         └──┘           └──┘            └┘                            
st       └────────────────┘└──────────────┘└───────────┘└──────────────────
393  
src  
typ  
doc  
txt  
par  
pid  
st   
394    theorem cast_pos [linear_ordered_semiring α] (n : pos_num) : 0 < (n : α) :=
id                       └─────────────────────┘        └─────┘           
src  ─┘                  └─────────────────────┘         └─────┘      
typ  ─┘                  └─────────────────────┘        └─────┘           
doc  ─┘                                                  └─────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
395    lt_of_lt_of_le zero_lt_one (one_le_cast n)
id     └────────────┘ └─────────┘  └─────────┘ 
src    └────────────┘ └─────────┘  └─────────┘
typ    └────────────┘ └─────────┘  └─────────┘ 
396  
397    @[simp] theorem cast_mul [semiring α] (m n) : ((m * n : pos_num) : α) = m * n :=
id                               └──────┘                  └─────┘         
src                              └──────┘                     └─────┘          
typ                              └──────┘                  └─────┘         
doc      └──┘                                                  └─────┘
398    by rw [← cast_to_nat, mul_to_nat, nat.cast_mul, cast_to_nat, cast_to_nat]
id              └─────────┘  └────────┘  └──────────┘  └─────────┘  └─────────┘
src       └────┘└─────────┘└┘└────────┘└┘└──────────┘└┘└─────────┘└┘└─────────┘└─
typ       └────┘└─────────┘└┘└────────┘└┘└──────────┘└┘└─────────┘└┘└─────────┘└─
doc       └────┘           └┘          └┘            └┘           └┘           └─
txt       └────┘           └┘          └┘            └┘           └┘           └─
par       └────┘           └┘          └┘            └┘           └┘           └─
pid         └──┘           └┘          └┘            └┘           └┘           
st       └────────────────┘└──────────┘└────────────┘└───────────┘└───────────┘
399  
src  
typ  
doc  
txt  
par  
pid  
st   
400    theorem cmp_eq (m n) : cmp m n = ordering.eq ↔ m = n :=
id                            └─┘    └─────────┘    
src  ─┘                       └─┘      └─────────┘    
typ  ─┘                       └─┘    └─────────┘    
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
401    begin
st     └─────
402      have := cmp_to_nat m n,
id               └────────┘  
src      └──────┘└────────┘ 
typ      └──────┘└────────┘
doc      └──────┘           
txt      └──────┘           
par      └──────┘           
pid      └───┘└─┘           
st   ─────────────────────────┘└─
403      cases cmp m n; simp at this ⊢; try {exact this};
id             └─┘                               └──┘
src      └────┘└─┘    └────────────┘  └───┘└────┘    
typ      └────┘└─┘  └────────────┘  └───┘└────┘└──┘
doc      └────┘       └────────────┘  └───┘└────┘    
txt      └────┘       └────────────┘  └───┘└────┘    
par      └────┘       └────────────┘  └───┘└────┘    
pid                      └───────┘     └──────┘    
st   ───────────────────────────────────────┘└────────┘└┘
404      { simp [show m ≠ n, from λ e, by rw e at this; exact lt_irrefl _ this] }
id                                                        └───────┘   └──┘
src        └────┘      └─────┘ └──┘  └─┘ └──────┘└┘└────┘└───────┘└─┘    └┘
typ        └────┘    └─────┘ └──┘  └─┘└──────┘└┘└────┘└───────┘└─┘└──┘└┘
doc        └────┘       └─────┘ └──┘  └─┘ └──────┘└┘└────┘         └─┘    └┘
txt        └────┘       └─────┘ └──┘  └─┘ └──────┘└┘└────┘         └─┘    └┘
par        └────┘       └─────┘ └──┘  └─┘ └──────┘└┘└────┘         └─┘    └┘
pid                   └─────┘ └──┘  └──┘ └──────────────┘         └─┘    
st   ───┘└──────────────────────────────┘└───────────────────────────────────┘└┘└─
405    end
st   ────┘
406  
407    @[simp] theorem cast_lt [linear_ordered_semiring α] {m n : pos_num} : (m:α) < n ↔ m < n :=
id                              └─────────────────────┘          └─────┘             
src                             └─────────────────────┘           └─────┘                
typ                             └─────────────────────┘          └─────┘             
doc      └──┘                                                     └─────┘
408    by rw [← cast_to_nat m, ← cast_to_nat n, nat.cast_lt, lt_to_nat]
id              └─────────┘     └─────────┘   └─────────┘  └───────┘
src       └────┘└─────────┘ └──┘└─────────┘ └┘└─────────┘└┘└───────┘└─
typ       └────┘└─────────┘└──┘└─────────┘└┘└─────────┘└┘└───────┘└─
doc       └────┘            └──┘            └┘           └┘         └─
txt       └────┘            └──┘            └┘           └┘         └─
par       └────┘            └──┘            └┘           └┘         └─
pid         └──┘            └──┘            └┘           └┘         
st       └──────────────────┘└───────────────┘└───────────┘└─────────┘
409  
src  
typ  
doc  
txt  
par  
pid  
st   
410    @[simp] theorem cast_le [linear_ordered_semiring α] {m n : pos_num} : (m:α) ≤ n ↔ m ≤ n :=
id                              └─────────────────────┘          └─────┘             
src  ─┘                         └─────────────────────┘           └─────┘                
typ  ─┘                         └─────────────────────┘          └─────┘             
doc  ─┘  └──┘                                                     └─────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
411    by rw ← not_lt; exact not_congr cast_lt
id             └────┘        └───────┘ └─────┘
src       └───┘└────┘  └────┘└───────┘└─────┘
typ       └───┘└────┘  └────┘└───────┘└─────┘
doc       └───┘        └────┘                
txt       └───┘        └────┘                
par       └───┘        └────┘                
pid         └─┘                             
st       └─────────────────────────────────────
412  
src  
typ  
doc  
txt  
par  
pid  
st   
413  end pos_num
414  
415  namespace num
416    variables {α : Type*}
417    open pos_num
418  
419    theorem bit_to_nat (b n) : (bit b n : ℕ) = nat.bit b n :=
id                                 └─┘        └─────┘  
src                                └─┘          └─────┘
typ                                └─┘        └─────┘  
420    by cases b; cases n; refl
id                      
src       └────┘   └────┘   └────
typ       └────┘  └────┘  └────
doc       └────┘   └────┘   └────
txt       └────┘   └────┘   └────
par       └────┘   └────┘   └────
pid                           
st       └───────────────────────
421  
src  
typ  
doc  
txt  
par  
pid  
st   
422    theorem cast_succ' [add_monoid α] [has_one α] (n) : (succ' n : α) = n + 1 :=
id                         └────────┘    └─────┘          └───┘        
src  ─┘                    └────────┘     └─────┘           └───┘           
typ  ─┘                    └────────┘    └─────┘          └───┘        
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
423    by rw [← pos_num.cast_to_nat, succ'_to_nat, nat.cast_add_one, cast_to_nat]
id              └─────────────────┘  └──────────┘  └──────────────┘  └─────────┘
src       └────┘└─────────────────┘└┘└──────────┘└┘└──────────────┘└┘└─────────┘└─
typ       └────┘└─────────────────┘└┘└──────────┘└┘└──────────────┘└┘└─────────┘└─
doc       └────┘                   └┘            └┘                └┘           └─
txt       └────┘                   └┘            └┘                └┘           └─
par       └────┘                   └┘            └┘                └┘           └─
pid         └──┘                   └┘            └┘                └┘           
st       └────────────────────────┘└────────────┘└────────────────┘└───────────┘
424  
src  
typ  
doc  
txt  
par  
pid  
st   
425    theorem cast_succ [add_monoid α] [has_one α] (n) : (succ n : α) = n + 1 := cast_succ' n
id                        └────────┘    └─────┘          └──┘              └────────┘ 
src  ─┘                   └────────┘     └─────┘           └──┘                 └────────┘
typ  ─┘                   └────────┘    └─────┘          └──┘              └────────┘ 
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
426  
427    @[simp] theorem cast_add [semiring α] (m n) : ((m + n : num) : α) = m + n :=
id                               └──────┘                  └─┘         
src                              └──────┘                     └─┘          
typ                              └──────┘                  └─┘         
doc      └──┘                                                  └─┘
428    by rw [← cast_to_nat, add_to_nat, nat.cast_add, cast_to_nat, cast_to_nat]
id              └─────────┘  └────────┘  └──────────┘  └─────────┘  └─────────┘
src       └────┘└─────────┘└┘└────────┘└┘└──────────┘└┘└─────────┘└┘└─────────┘└─
typ       └────┘└─────────┘└┘└────────┘└┘└──────────┘└┘└─────────┘└┘└─────────┘└─
doc       └────┘           └┘          └┘            └┘           └┘           └─
txt       └────┘           └┘          └┘            └┘           └┘           └─
par       └────┘           └┘          └┘            └┘           └┘           └─
pid         └──┘           └┘          └┘            └┘           └┘           
st       └────────────────┘└──────────┘└────────────┘└───────────┘└───────────┘
429  
src  
typ  
doc  
txt  
par  
pid  
st   
430    @[simp] theorem cast_bit0 [semiring α] (n : num) : (n.bit0 : α) = _root_.bit0 n :=
id                                └──────┘        └─┘     └───┘      └─────────┘ 
src  ─┘                           └──────┘         └─┘      └───┘       └─────────┘
typ  ─┘                           └──────┘        └─┘     └───┘      └─────────┘ 
doc  ─┘  └──┘                                      └─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
431    by rw [← bit0_of_bit0, _root_.bit0, cast_add]; refl
id              └──────────┘  └─────────┘  └──────┘
src       └────┘└──────────┘└┘└─────────┘└┘└──────┘  └────
typ       └────┘└──────────┘└┘└─────────┘└┘└──────┘  └────
doc       └────┘            └┘           └┘          └────
txt       └────┘            └┘           └┘          └────
par       └────┘            └┘           └┘          └────
pid         └──┘            └┘           └┘              
st       └─────────────────┘└───────────┘└────────┘└──────
432  
src  
typ  
doc  
txt  
par  
pid  
st   
433    @[simp] theorem cast_bit1 [semiring α] (n : num) : (n.bit1 : α) = _root_.bit1 n :=
id                                └──────┘        └─┘     └───┘      └─────────┘ 
src  ─┘                           └──────┘         └─┘      └───┘       └─────────┘
typ  ─┘                           └──────┘        └─┘     └───┘      └─────────┘ 
doc  ─┘  └──┘                                      └─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
434    by rw [← bit1_of_bit1, _root_.bit1, bit0_of_bit0, cast_add, cast_bit0]; refl
id              └──────────┘  └─────────┘  └──────────┘  └──────┘  └───────┘
src       └────┘└──────────┘└┘└─────────┘└┘└──────────┘└┘└──────┘└┘└───────┘  └────
typ       └────┘└──────────┘└┘└─────────┘└┘└──────────┘└┘└──────┘└┘└───────┘  └────
doc       └────┘            └┘           └┘            └┘        └┘           └────
txt       └────┘            └┘           └┘            └┘        └┘           └────
par       └────┘            └┘           └┘            └┘        └┘           └────
pid         └──┘            └┘           └┘            └┘        └┘               
st       └─────────────────┘└───────────┘└────────────┘└────────┘└─────────┘└──────
435  
src  
typ  
doc  
txt  
par  
pid  
st   
436    @[simp] theorem cast_mul [semiring α] : ∀ m n, ((m * n : num) : α) = m * n
id                               └──────┘                 └─┘         
src  ─┘                          └──────┘                      └─┘          
typ  ─┘                          └──────┘                 └─┘         
doc  ─┘  └──┘                                                   └─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
437    | 0       0       := (zero_mul _).symm
id                           └──────┘   └──┘
src                          └──────┘   └──┘
typ                          └──────┘   └──┘
438    | 0       (pos q) := (zero_mul _).symm
id                └─┘        └──────┘   └──┘
src               └─┘        └──────┘   └──┘
typ               └─┘        └──────┘   └──┘
439    | (pos p) 0       := (mul_zero _).symm
id        └─┘                └──────┘   └──┘
src       └─┘                └──────┘   └──┘
typ       └─┘                └──────┘   └──┘
440    | (pos p) (pos q) := pos_num.cast_mul _ _
id                └─┘       └──────────────┘
src               └─┘       └──────────────┘
typ               └─┘       └──────────────┘
441  
442    theorem size_to_nat : ∀ n, (size n : ℕ) = nat.size n
id                                └──┘       └──────┘ 
src                                └──┘        └──────┘
typ                               └──┘       └──────┘ 
443    | 0       := nat.size_zero.symm
id                  └───────────┘└───┘
src                 └───────────┘└───┘
typ                 └───────────┘└───┘
444    | (pos p) := p.size_to_nat
id        └─┘       └──────────┘
src       └─┘        └──────────┘
typ       └─┘       └──────────┘
445  
446    theorem size_eq_nat_size : ∀ n, (size n : ℕ) = nat_size n
id                                     └──┘       └──────┘ 
src                                     └──┘        └──────┘
typ                                    └──┘       └──────┘ 
447    | 0       := rfl
id                  └─┘
src                 └─┘
typ                 └─┘
448    | (pos p) := p.size_eq_nat_size
id        └─┘       └───────────────┘
src       └─┘        └───────────────┘
typ       └─┘       └───────────────┘
449  
450    theorem nat_size_to_nat (n) : nat_size n = nat.size n :=
id                                   └──────┘   └──────┘ 
src                                  └──────┘    └──────┘
typ                                  └──────┘   └──────┘ 
451    by rw [← size_eq_nat_size, size_to_nat]
id              └──────────────┘  └─────────┘
src       └────┘└──────────────┘└┘└─────────┘└─
typ       └────┘└──────────────┘└┘└─────────┘└─
doc       └────┘                └┘           └─
txt       └────┘                └┘           └─
par       └────┘                └┘           └─
pid         └──┘                └┘           
st       └─────────────────────┘└───────────┘
452  
src  
typ  
doc  
txt  
par  
pid  
st   
453    @[simp] theorem of_nat'_eq : ∀ n, num.of_nat' n = n :=
id                                      └─────────┘   
src  ─┘                                  └─────────┘   
typ  ─┘                                 └─────────┘   
doc  ─┘  └──┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
454    nat.binary_rec rfl $ λ b n IH, begin
id     └────────────┘ └─┘       └┘
src    └────────────┘ └─┘
typ    └────────────┘ └─┘       └┘
st                                    └─────
455      rw of_nat' at IH ⊢,
id          └─────┘
src      └─┘└─────┘└──────┘
typ      └─┘└─────┘└──────┘
doc      └─┘       └──────┘
txt      └─┘       └──────┘
par      └─┘       └──────┘
pid               └──────┘
st   ─────────────────────┘└─
456      rw [nat.binary_rec_eq, IH],
id           └───────────────┘  └┘
src      └──┘└───────────────┘└┘  
typ      └──┘└───────────────┘└┘└┘
doc      └──┘                 └┘  
txt      └──┘                 └┘  
par      └──┘                 └┘  
pid        └┘                 └┘  
st   ────────────────────────┘└──┘└──
457      { cases b; simp [nat.bit, bit0_of_bit0, bit1_of_bit1] },
id                       └─────┘  └──────────┘  └──────────┘
src        └────┘   └────┘└─────┘└┘└──────────┘└┘└──────────┘└┘
typ        └────┘  └────┘└─────┘└┘└──────────┘└┘└──────────┘└┘
doc        └────┘   └────┘       └┘            └┘            └┘
txt        └────┘   └────┘       └┘            └┘            └┘
par        └────┘   └────┘       └┘            └┘            └┘
pid                           └┘            └┘            
st   ─────┘└──────────────────────────────────────────────────┘└┘
458      { refl }
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid            
st   ──────────┘└─
459    end
st   ────┘
460  
461    theorem zneg_to_znum (n : num) : -n.to_znum = n.to_znum_neg := by cases n; refl
id                               └─┘    └──────┘  └──────────┘             
src                              └─┘     └──────┘   └──────────┘       └────┘   └────
typ                              └─┘    └──────┘  └──────────┘       └────┘  └────
doc                              └─┘                                     └────┘   └────
txt                                                                      └────┘   └────
par                                                                      └────┘   └────
pid                                                                                  
st                                                                      └──────────────
462    theorem zneg_to_znum_neg (n : num) : -n.to_znum_neg = n.to_znum := by cases n; refl
id                                   └─┘    └──────────┘  └──────┘             
src  ─┘                              └─┘     └──────────┘   └──────┘       └────┘   └────
typ  ─┘                              └─┘    └──────────┘  └──────┘       └────┘  └────
doc  ─┘                              └─┘                                     └────┘   └────
txt  ─┘                                                                      └────┘   └────
par  ─┘                                                                      └────┘   └────
pid  ─┘                                                                                  
st   ─┘                                                                     └──────────────
463  
src  
typ  
doc  
txt  
par  
pid  
st   
464    theorem to_znum_inj {m n : num} : m.to_znum = n.to_znum ↔ m = n :=
id                                └─┘    └──────┘  └──────┘    
src  ─┘                           └─┘     └──────┘   └──────┘    
typ  ─┘                           └─┘    └──────┘  └──────┘    
doc  ─┘                           └─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
465    ⟨λ h, by cases m; cases n; cases h; refl, congr_arg _⟩
id                                           └───────┘
src             └────┘   └────┘   └────┘   └──┘  └───────┘
typ            └────┘  └────┘  └────┘  └──┘  └───────┘
doc             └────┘   └────┘   └────┘   └──┘
txt             └────┘   └────┘   └────┘   └──┘
par             └────┘   └────┘   └────┘   └──┘
pid                                  
st             └──────────────────────────────┘
466  
467    @[simp] theorem cast_to_znum [has_zero α] [has_one α] [has_add α] [has_neg α] :
id                                   └──────┘    └─────┘    └─────┘    └─────┘ 
src                                  └──────┘     └─────┘     └─────┘     └─────┘
typ                                  └──────┘    └─────┘    └─────┘    └─────┘ 
doc      └──┘
468      ∀ n : num, (n.to_znum : α) = n
id            └─┘   └──────┘      
src            └─┘    └──────┘      
typ           └─┘   └──────┘      
doc            └─┘
469    | 0           := rfl
id                      └─┘
src                     └─┘
typ                     └─┘
470    | (num.pos p) := rfl
id        └─────┘       └─┘
src       └─────┘       └─┘
typ       └─────┘       └─┘
471  
472    @[simp] theorem cast_to_znum_neg [add_group α] [has_one α] :
id                                       └───────┘    └─────┘ 
src                                      └───────┘     └─────┘
typ                                      └───────┘    └─────┘ 
doc      └──┘
473      ∀ n : num, (n.to_znum_neg : α) = -n
id            └─┘   └──────────┘      
src            └─┘    └──────────┘       
typ           └─┘   └──────────┘      
doc            └─┘
474    | 0           := neg_zero.symm
id                      └──────┘└───┘
src                     └──────┘└───┘
typ                     └──────┘└───┘
475    | (num.pos p) := rfl
id        └─────┘       └─┘
src       └─────┘       └─┘
typ       └─────┘       └─┘
476  
477    @[simp] theorem add_to_znum (m n : num) : num.to_znum (m + n) = m.to_znum + n.to_znum :=
id                                        └─┘    └─────────┘       └──────┘  └──────┘
src                                       └─┘    └─────────┘          └──────┘   └──────┘
typ                                       └─┘    └─────────┘       └──────┘  └──────┘
doc      └──┘                             └─┘
478    by cases m; cases n; refl
id                      
src       └────┘   └────┘   └────
typ       └────┘  └────┘  └────
doc       └────┘   └────┘   └────
txt       └────┘   └────┘   └────
par       └────┘   └────┘   └────
pid                           
st       └───────────────────────
479  
src  
typ  
doc  
txt  
par  
pid  
st   
480  end num
481  
482  namespace pos_num
483    open num
484  
485    theorem pred_to_nat {n : pos_num} (h : n > 1) : (pred n : ℕ) = nat.pred n :=
id                              └─────┘               └──┘       └──────┘ 
src                             └─────┘                └──┘        └──────┘
typ                             └─────┘               └──┘       └──────┘ 
doc                             └─────┘
486    begin
st     └─────
487      unfold pred,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid            └───┘
st   ──────────────┘└─
488      have := pred'_to_nat n,
id               └──────────┘ 
src      └──────┘└──────────┘
typ      └──────┘└──────────┘
doc      └──────┘            
txt      └──────┘            
par      └──────┘            
pid      └───┘└─┘            
st   ─────────────────────────┘└─
489      cases e : pred' n,
id                 └───┘ 
src      └────┘ └─┘└───┘
typ      └────┘ └─┘└───┘
doc      └────┘ └─┘     
txt      └────┘ └─┘     
par      └────┘ └─┘     
pid            └─┘     
st   ────────────────────┘└─
490      { have : (1:ℕ) ≤ nat.pred n :=
id                       └──────┘ 
src        └─────┘ └┘ └┘└──────┘ └───
typ        └─────┘ └┘ └┘└──────┘└───
doc        └─────┘ └┘ └┘          └───
txt        └─────┘ └┘ └┘          └───
par        └─────┘ └┘ └┘          └───
pid        └───┘└┘ └┘ └┘          └───
st   ─────┘└────────────────────────────
491          nat.pred_le_pred ((@cast_lt ℕ _ _ _).2 h),
id           └──────────────┘    └─────┘            
src  ───────┘└──────────────┘   └─────┘ └────────┘ 
typ  ───────┘└──────────────┘   └─────┘ └────────┘
doc  ───────┘                           └────────┘ 
txt  ───────┘                           └────────┘ 
par  ───────┘                           └────────┘ 
pid  ───────┘                           └────────┘ 
st   ────────────────────────────────────────────────┘└─
492        rw [← pred'_to_nat, e] at this,
id               └──────────┘  
src        └────┘└──────────┘└┘ └───────┘
typ        └────┘└──────────┘└┘└───────┘
doc        └────┘            └┘ └───────┘
txt        └────┘            └┘ └───────┘
par        └────┘            └┘ └───────┘
pid          └──┘            └┘ └──────┘
st   ───────────────────────┘└─┘└──────┘└─
493        exact absurd this dec_trivial },
id               └────┘ └──┘ └─────────┘
src        └────┘└────┘    └─────────┘
typ        └────┘└────┘└──┘└─────────┘
doc        └────┘          └─────────┘
txt        └────┘                     
par        └────┘                     
pid                                  
st   ───────────────────────────────────┘└┘
494      { rw [← pred'_to_nat, e], refl }
id               └──────────┘  
src        └────┘└──────────┘└┘   └───┘
typ        └────┘└──────────┘└┘  └───┘
doc        └────┘            └┘   └───┘
txt        └────┘            └┘   └───┘
par        └────┘            └┘   └───┘
pid          └──┘            └┘       
st   ───────────────────────┘└─┘└─────┘└─
495    end
st   ────┘
496  
497    theorem sub'_one (a : pos_num) : sub' a 1 = (pred' a).to_znum :=
id                           └─────┘    └──┘      └───┘  └─────┘
src                          └─────┘    └──┘       └───┘   └─────┘
typ                          └─────┘    └──┘      └───┘  └─────┘
doc                          └─────┘
498    by cases a; refl
id              
src       └────┘   └────
typ       └────┘  └────
doc       └────┘   └────
txt       └────┘   └────
par       └────┘   └────
pid                   
st       └──────────────
499  
src  
typ  
doc  
txt  
par  
pid  
st   
500    theorem one_sub' (a : pos_num) : sub' 1 a = (pred' a).to_znum_neg :=
id                           └─────┘    └──┘      └───┘  └─────────┘
src  ─┘                      └─────┘    └──┘       └───┘   └─────────┘
typ  ─┘                      └─────┘    └──┘      └───┘  └─────────┘
doc  ─┘                      └─────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
501    by cases a; refl
id              
src       └────┘   └────
typ       └────┘  └────
doc       └────┘   └────
txt       └────┘   └────
par       └────┘   └────
pid                   
st       └──────────────
502  
src  
typ  
doc  
txt  
par  
pid  
st   
503    theorem lt_iff_cmp {m n} : m < n ↔ cmp m n = ordering.lt := iff.rfl
id                                    └─┘    └─────────┘    └─────┘
src  ─┘                                 └─┘      └─────────┘    └─────┘
typ  ─┘                               └─┘    └─────────┘    └─────┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
504  
505    theorem le_iff_cmp {m n} : m ≤ n ↔ cmp m n ≠ ordering.gt :=
id                                    └─┘    └─────────┘
src                                     └─┘      └─────────┘
typ                                   └─┘    └─────────┘
506    not_congr $ lt_iff_cmp.trans $
id     └───────┘   └────────┘└────┘
src    └───────┘   └────────┘└────┘
typ    └───────┘   └────────┘└────┘
507    by rw ← cmp_swap; cases cmp m n; exact dec_trivial
id             └──────┘        └─┘          └─────────┘
src       └───┘└──────┘  └────┘└─┘    └────┘└─────────┘
typ       └───┘└──────┘  └────┘└─┘  └────┘└─────────┘
doc       └───┘          └────┘       └────┘└─────────┘
txt       └───┘          └────┘       └────┘           
par       └───┘          └────┘       └────┘           
pid         └─┘                                      
st       └────────────────────────────────────────────────
508  
src  
typ  
doc  
txt  
par  
pid  
st   
509  end pos_num
510  
511  namespace num
512    variables {α : Type*}
513    open pos_num
514  
515    theorem pred_to_nat : ∀ (n : num), (pred n : ℕ) = nat.pred n
id                                 └─┘    └──┘       └──────┘ 
src                                 └─┘    └──┘        └──────┘
typ                                └─┘    └──┘       └──────┘ 
doc                                 └─┘
516    | 0       := rfl
id                  └─┘
src                 └─┘
typ                 └─┘
517    | (pos p) := by rw [pred, pos_num.pred'_to_nat]; refl
id        └─┘              └──┘  └──────────────────┘
src       └─┘          └──┘└──┘└┘└──────────────────┘  └────
typ       └─┘          └──┘└──┘└┘└──────────────────┘  └────
doc                    └──┘    └┘                      └────
txt                    └──┘    └┘                      └────
par                    └──┘    └┘                      └────
pid                      └┘    └┘                          
st                    └───────┘└────────────────────┘└──────
518  
src  
typ  
doc  
txt  
par  
pid  
st   
519    theorem ppred_to_nat : ∀ (n : num), coe <$> ppred n = nat.ppred n
id                                  └─┘   └─┘ └─┘ └───┘   └───────┘ 
src  ─┘                              └─┘   └─┘ └─┘ └───┘    └───────┘
typ  ─┘                             └─┘   └─┘ └─┘ └───┘   └───────┘ 
doc  ─┘                              └─┘                     └───────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
520    | 0       := rfl
id                  └─┘
src                 └─┘
typ                 └─┘
521    | (pos p) := by rw [ppred, option.map_some, nat.ppred_eq_some.2];
id        └─┘              └───┘  └─────────────┘  └───────────────┘
src       └─┘          └──┘└───┘└┘└─────────────┘└┘└───────────────┘└─┘
typ       └─┘          └──┘└───┘└┘└─────────────┘└┘└───────────────┘└─┘
doc                    └──┘     └┘               └┘                 └─┘
txt                    └──┘     └┘               └┘                 └─┘
par                    └──┘     └┘               └┘                 └─┘
pid                      └┘     └┘               └┘                 └─┘
st                    └────────┘└───────────────┘└─────────────────┘└─┘└─
522      rw [pos_num.pred'_to_nat, nat.succ_pred_eq_of_pos (pos_num.to_nat_pos _)]; refl
id           └──────────────────┘  └─────────────────────┘  └────────────────┘
src      └──┘└──────────────────┘└┘└─────────────────────┘ └────────────────┘└──┘  └────
typ      └──┘└──────────────────┘└┘└─────────────────────┘ └────────────────┘└──┘  └────
doc      └──┘                    └┘                                          └──┘  └────
txt      └──┘                    └┘                                          └──┘  └────
par      └──┘                    └┘                                          └──┘  └────
pid        └┘                    └┘                                          └──┘      
st   ───────┘└──────────────────┘└──────────────────────────────────────────────┘└──────
523  
src  
typ  
doc  
txt  
par  
pid  
st   
524    theorem cmp_swap (m n) : (cmp m n).swap = cmp n m :=
id                               └─┘   └──┘   └─┘  
src  ─┘                          └─┘     └──┘   └─┘
typ  ─┘                          └─┘   └──┘   └─┘  
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
525    by cases m; cases n; try {unfold cmp}; try {refl}; apply pos_num.cmp_swap
id                                                            └──────────────┘
src       └────┘   └────┘   └───┘└────────┘  └───┘└──┘  └────┘└──────────────┘
typ       └────┘  └────┘  └───┘└────────┘  └───┘└──┘  └────┘└──────────────┘
doc       └────┘   └────┘   └───┘└────────┘  └───┘└──┘  └────┘                
txt       └────┘   └────┘   └───┘└────────┘  └───┘└──┘  └────┘                
par       └────┘   └────┘   └───┘└────────┘  └───┘└──┘  └────┘                
pid                          └───────────┘     └─────┘                       
st       └──────────────────────┘└────────┘└┘└────┘└──┘└┘└───────────────────────
526  
src  
typ  
doc  
txt  
par  
pid  
st   
527    theorem cmp_eq (m n) : cmp m n = ordering.eq ↔ m = n :=
id                            └─┘    └─────────┘    
src  ─┘                       └─┘      └─────────┘    
typ  ─┘                       └─┘    └─────────┘    
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
528    begin
st     └─────
529      have := cmp_to_nat m n,
id               └────────┘  
src      └──────┘└────────┘ 
typ      └──────┘└────────┘
doc      └──────┘           
txt      └──────┘           
par      └──────┘           
pid      └───┘└─┘           
st   ─────────────────────────┘└─
530      cases cmp m n; simp at this ⊢; try {exact this};
id             └─┘                               └──┘
src      └────┘└─┘    └────────────┘  └───┘└────┘    
typ      └────┘└─┘  └────────────┘  └───┘└────┘└──┘
doc      └────┘       └────────────┘  └───┘└────┘    
txt      └────┘       └────────────┘  └───┘└────┘    
par      └────┘       └────────────┘  └───┘└────┘    
pid                      └───────┘     └──────┘    
st   ───────────────────────────────────────┘└────────┘└┘
531      { simp [show m ≠ n, from λ e, by rw e at this; exact lt_irrefl _ this] }
id                                                        └───────┘   └──┘
src        └────┘      └─────┘ └──┘  └─┘ └──────┘└┘└────┘└───────┘└─┘    └┘
typ        └────┘    └─────┘ └──┘  └─┘└──────┘└┘└────┘└───────┘└─┘└──┘└┘
doc        └────┘       └─────┘ └──┘  └─┘ └──────┘└┘└────┘         └─┘    └┘
txt        └────┘       └─────┘ └──┘  └─┘ └──────┘└┘└────┘         └─┘    └┘
par        └────┘       └─────┘ └──┘  └─┘ └──────┘└┘└────┘         └─┘    └┘
pid                   └─────┘ └──┘  └──┘ └──────────────┘         └─┘    
st   ───┘└──────────────────────────────┘└───────────────────────────────────┘└┘└─
532    end
st   ────┘
533  
534    @[simp] theorem cast_lt [linear_ordered_semiring α] {m n : num} : (m:α) < n ↔ m < n :=
id                              └─────────────────────┘          └─┘             
src                             └─────────────────────┘           └─┘                
typ                             └─────────────────────┘          └─┘             
doc      └──┘                                                     └─┘
535    by rw [← cast_to_nat m, ← cast_to_nat n, nat.cast_lt, lt_to_nat]
id              └─────────┘     └─────────┘   └─────────┘  └───────┘
src       └────┘└─────────┘ └──┘└─────────┘ └┘└─────────┘└┘└───────┘└─
typ       └────┘└─────────┘└──┘└─────────┘└┘└─────────┘└┘└───────┘└─
doc       └────┘            └──┘            └┘           └┘         └─
txt       └────┘            └──┘            └┘           └┘         └─
par       └────┘            └──┘            └┘           └┘         └─
pid         └──┘            └──┘            └┘           └┘         
st       └──────────────────┘└───────────────┘└───────────┘└─────────┘
536  
src  
typ  
doc  
txt  
par  
pid  
st   
537    @[simp] theorem cast_le [linear_ordered_semiring α] {m n : num} : (m:α) ≤ n ↔ m ≤ n :=
id                              └─────────────────────┘          └─┘             
src  ─┘                         └─────────────────────┘           └─┘                
typ  ─┘                         └─────────────────────┘          └─┘             
doc  ─┘  └──┘                                                     └─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
538    by rw ← not_lt; exact not_congr cast_lt
id             └────┘        └───────┘ └─────┘
src       └───┘└────┘  └────┘└───────┘└─────┘
typ       └───┘└────┘  └────┘└───────┘└─────┘
doc       └───┘        └────┘                
txt       └───┘        └────┘                
par       └───┘        └────┘                
pid         └─┘                             
st       └─────────────────────────────────────
539  
src  
typ  
doc  
txt  
par  
pid  
st   
540    @[simp] theorem cast_inj [linear_ordered_semiring α] {m n : num} : (m:α) = n ↔ m = n :=
id                               └─────────────────────┘          └─┘             
src  ─┘                          └─────────────────────┘           └─┘                
typ  ─┘                          └─────────────────────┘          └─┘             
doc  ─┘  └──┘                                                      └─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
541    by rw [← cast_to_nat m, ← cast_to_nat n, nat.cast_inj, to_nat_inj]
id              └─────────┘     └─────────┘   └──────────┘  └────────┘
src       └────┘└─────────┘ └──┘└─────────┘ └┘└──────────┘└┘└────────┘└─
typ       └────┘└─────────┘└──┘└─────────┘└┘└──────────┘└┘└────────┘└─
doc       └────┘            └──┘            └┘            └┘          └─
txt       └────┘            └──┘            └┘            └┘          └─
par       └────┘            └──┘            └┘            └┘          └─
pid         └──┘            └──┘            └┘            └┘          
st       └──────────────────┘└───────────────┘└────────────┘└──────────┘
542  
src  
typ  
doc  
txt  
par  
pid  
st   
543    theorem lt_iff_cmp {m n} : m < n ↔ cmp m n = ordering.lt := iff.rfl
id                                    └─┘    └─────────┘    └─────┘
src  ─┘                                 └─┘      └─────────┘    └─────┘
typ  ─┘                               └─┘    └─────────┘    └─────┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
544  
545    theorem le_iff_cmp {m n} : m ≤ n ↔ cmp m n ≠ ordering.gt :=
id                                    └─┘    └─────────┘
src                                     └─┘      └─────────┘
typ                                   └─┘    └─────────┘
546    not_congr $ lt_iff_cmp.trans $
id     └───────┘   └────────┘└────┘
src    └───────┘   └────────┘└────┘
typ    └───────┘   └────────┘└────┘
547    by rw ← cmp_swap; cases cmp m n; exact dec_trivial
id             └──────┘        └─┘          └─────────┘
src       └───┘└──────┘  └────┘└─┘    └────┘└─────────┘
typ       └───┘└──────┘  └────┘└─┘  └────┘└─────────┘
doc       └───┘          └────┘       └────┘└─────────┘
txt       └───┘          └────┘       └────┘           
par       └───┘          └────┘       └────┘           
pid         └─┘                                      
st       └────────────────────────────────────────────────
548  
src  
typ  
doc  
txt  
par  
pid  
st   
549    theorem bitwise_to_nat {f : num → num → num} {g : bool → bool → bool}
id                                 └─┘   └─┘   └─┘       └──┘   └──┘   └──┘
src  ─┘                            └─┘   └─┘   └─┘       └──┘   └──┘   └──┘
typ  ─┘                            └─┘   └─┘   └─┘       └──┘   └──┘   └──┘
doc  ─┘                            └─┘   └─┘   └─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
550      (p : pos_num → pos_num → num)
id            └─────┘   └─────┘   └─┘
src           └─────┘   └─────┘   └─┘
typ           └─────┘   └─────┘   └─┘
doc           └─────┘   └─────┘   └─┘
551      (gff : g ff ff = ff)
id               └┘ └┘  └┘
src               └┘ └┘  └┘
typ              └┘ └┘  └┘
552      (f00 : f 0 0 = 0)
id                   
src                   
typ                  
553      (f0n : ∀ n, f 0 (pos n) = cond (g ff tt) (pos n) 0)
id                      └─┘    └──┘   └┘ └┘   └─┘ 
src                       └─┘     └──┘    └┘ └┘   └─┘
typ                     └─┘    └──┘   └┘ └┘   └─┘ 
554      (fn0 : ∀ n, f (pos n) 0 = cond (g tt ff) (pos n) 0)
id                    └─┘      └──┘   └┘ └┘   └─┘ 
src                     └─┘       └──┘    └┘ └┘   └─┘
typ                   └─┘      └──┘   └┘ └┘   └─┘ 
555      (fnn : ∀ m n, f (pos m) (pos n) = p m n)
id                     └─┘    └─┘      
src                       └─┘     └─┘    
typ                    └─┘    └─┘      
556      (p11 : p 1 1 = cond (g tt tt) 1 0)
id                    └──┘   └┘ └┘
src                    └──┘    └┘ └┘
typ                   └──┘   └┘ └┘
557      (p1b : ∀ b n, p 1 (pos_num.bit b n) = bit (g tt b) (cond (g ff tt) (pos n) 0))
id                       └─────────┘     └─┘   └┘    └──┘   └┘ └┘   └─┘ 
src                         └─────────┘       └─┘    └┘     └──┘    └┘ └┘   └─┘
typ                      └─────────┘     └─┘   └┘    └──┘   └┘ └┘   └─┘ 
558      (pb1 : ∀ a m, p (pos_num.bit a m) 1 = bit (g a tt) (cond (g tt ff) (pos m) 0))
id                     └─────────┘       └─┘    └┘   └──┘   └┘ └┘   └─┘ 
src                       └─────────┘         └─┘      └┘   └──┘    └┘ └┘   └─┘
typ                    └─────────┘       └─┘    └┘   └──┘   └┘ └┘   └─┘ 
559      (pbb : ∀ a b m n, p (pos_num.bit a m) (pos_num.bit b n) = bit (g a b) (p m n))
id                       └─────────┘     └─────────┘     └─┘         
src                           └─────────┘       └─────────┘       └─┘
typ                      └─────────┘     └─────────┘     └─┘         
560      : ∀ m n : num, (f m n : ℕ) = nat.bitwise g m n :=
id                 └─┘           └─────────┘   
src                └─┘              └─────────┘
typ                └─┘           └─────────┘   
doc                └─┘
561    begin
st     └─────
562      intros, cases m with m; cases n with n;
id                                    
src      └────┘  └────┘ └─────┘  └────┘ └─────┘
typ      └────┘  └────┘└─────┘  └────┘└─────┘
doc      └────┘  └────┘ └─────┘  └────┘ └─────┘
txt      └────┘  └────┘ └─────┘  └────┘ └─────┘
par      └────┘  └────┘ └─────┘  └────┘ └─────┘
pid                    └─────┘        └─────┘
st   ─────────┘└─────────────────────────────────
563      try { change zero with 0 };
id                    └──┘
src      └────┘└─────┘└──┘└──────┘
typ      └────┘└─────┘└──┘└──────┘
doc      └────┘└─────┘    └──────┘
txt      └────┘└─────┘    └──────┘
par      └────┘└─────┘    └──────┘
pid         └────────┘    └───────┘
st   ────────┘└──────────────────┘└┘
564      try { change ((0:num):ℕ) with 0 },
id                        └─┘
src      └────┘└─────┘  └┘└─┘└┘ └───────┘
typ      └────┘└─────┘  └┘└─┘└┘ └───────┘
doc      └────┘└─────┘  └┘└─┘└┘ └───────┘
txt      └────┘└─────┘  └┘   └┘ └───────┘
par      └────┘└─────┘  └┘   └┘ └───────┘
pid         └────────┘  └┘   └┘ └────────┘
st   ────────┘└─────────────────────────┘└┘
565      { rw [f00, nat.bitwise_zero]; refl },
id             └─┘  └──────────────┘
src        └──┘   └┘└──────────────┘  └───┘
typ        └──┘└─┘└┘└──────────────┘  └───┘
doc        └──┘   └┘                  └───┘
txt        └──┘   └┘                  └───┘
par        └──┘   └┘                  └───┘
pid          └┘   └┘                      
st   ─────┘└─────┘└────────────────┘└─────┘└┘
566      { unfold nat.bitwise, rw [f0n, nat.binary_rec_zero],
id                                 └─┘  └─────────────────┘
src        └────────────────┘  └──┘   └┘└─────────────────┘
typ        └────────────────┘  └──┘└─┘└┘└─────────────────┘
doc        └────────────────┘  └──┘   └┘                   
txt        └────────────────┘  └──┘   └┘                   
par        └────────────────┘  └──┘   └┘                   
pid              └──────────┘    └┘   └┘                   
st   ─────┘└────────────────┘└───────┘└───────────────────┘└──
567        cases g ff tt; refl },
id                └┘ └┘
src        └────┘ └┘└┘  └───┘
typ        └────┘└┘└┘  └───┘
doc        └────┘       └───┘
txt        └────┘       └───┘
par        └────┘       └───┘
pid                        
st   ─────────────────────────┘└┘
568      { unfold nat.bitwise,
src        └────────────────┘
typ        └────────────────┘
doc        └────────────────┘
txt        └────────────────┘
par        └────────────────┘
pid              └──────────┘
st   ─────┘└────────────────┘└─
569        generalize h : (pos m : ℕ) = m', revert h,
id                         └─┘ 
src        └─────────────┘ └─┘ └─┘ └┘     └──────┘
typ        └─────────────┘ └─┘└─┘ └┘     └──────┘
doc        └─────────────┘     └─┘ └┘     └──────┘
txt        └─────────────┘     └─┘ └┘     └──────┘
par        └─────────────┘     └─┘ └┘     └──────┘
pid                  └┘└┘     └─┘ └┘           └┘
st   ────────────────────────────────────┘└────────┘└─
570        apply nat.bit_cases_on m' _, intros b m' h,
id               └──────────────┘ └┘
src        └────┘└──────────────┘  └┘  └───────────┘
typ        └────┘└──────────────┘└┘└┘  └───────────┘
doc        └────┘                  └┘  └───────────┘
txt        └────┘                  └┘  └───────────┘
par        └────┘                  └┘  └───────────┘
pid                               └┘        └─────┘
st   ────────────────────────────────┘└─────────────┘└─
571        rw [fn0, nat.binary_rec_eq, nat.binary_rec_zero, ←h],
id             └─┘  └───────────────┘  └─────────────────┘   
src        └──┘   └┘└───────────────┘└┘└─────────────────┘└─┘ 
typ        └──┘└─┘└┘└───────────────┘└┘└─────────────────┘└─┘
doc        └──┘   └┘                 └┘                   └─┘ 
txt        └──┘   └┘                 └┘                   └─┘ 
par        └──┘   └┘                 └┘                   └─┘ 
pid          └┘   └┘                 └┘                   └─┘ 
st   ────────────┘└─────────────────┘└───────────────────┘└──┘└─
572        cases g tt ff; refl,
id                └┘ └┘
src        └────┘ └┘└┘  └──┘
typ        └────┘└┘└┘  └──┘
doc        └────┘       └──┘
txt        └────┘       └──┘
par        └────┘       └──┘
pid                
st   ────────────────────────┘└─
573        apply nat.bitwise_bit_aux gff },
id               └─────────────────┘ └─┘
src        └────┘└─────────────────┘   
typ        └────┘└─────────────────┘└─┘
doc        └────┘                      
txt        └────┘                      
par        └────┘                      
pid                                   
st   ───────────────────────────────────┘└┘
574      { rw fnn,
id            └─┘
src        └─┘
typ        └─┘└─┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ───────────┘└─
575        have : ∀b (n : pos_num), (cond b ↑n 0 : ℕ) = ↑(cond b (pos n) 0 : num) :=
id                        └─────┘                        └──┘    └─┘        └─┘
src        └─────┘ └─────┘└─────┘        └───┘ └┘   └──┘  └─┘ └────┘└─┘└────
typ        └─────┘ └─────┘└─────┘        └───┘ └┘   └──┘  └─┘ └────┘└─┘└────
doc        └─────┘ └─────┘└─────┘         └───┘ └┘             └────┘└─┘└────
txt        └─────┘ └─────┘                └───┘ └┘             └────┘   └────
par        └─────┘ └─────┘                └───┘ └┘             └────┘   └────
pid        └───┘└┘ └─────┘                └───┘ └┘             └────┘   └───
st   ────────────────────────────────────────────────────────────────────────────────
576          by intros; cases b; refl,
id                            
src  ───────┘  └────┘└┘└────┘ └┘└──┘
typ  ───────┘  └────┘└┘└────┘└┘└──┘
doc  ───────┘  └────┘└┘└────┘ └┘└──┘
txt  ───────┘  └────┘└┘└────┘ └┘└──┘
par  ───────┘  └────┘└┘└────┘ └┘└──┘
pid  ───────┘  └─────────────┘ └────┘
st   ─────────┘└────────────────────┘└─
577        induction m with m IH m IH generalizing n; cases n with n n,
id                                                         
src        └────────┘ └────────────────────────────┘  └────┘ └───────┘
typ        └────────┘└────────────────────────────┘  └────┘└───────┘
doc        └────────┘ └────────────────────────────┘  └────┘ └───────┘
txt        └────────┘ └────────────────────────────┘  └────┘ └───────┘
par        └────────┘ └────────────────────────────┘  └────┘ └───────┘
pid                  └────────────┘└─────────────┘        └───────┘
st   ────────────────────────────────────────────────────────────────┘└─
578        any_goals { change one with 1 },
id                            └─┘
src        └──────────┘└─────┘└─┘└──────┘
typ        └──────────┘└─────┘└─┘└──────┘
doc        └──────────┘└─────┘   └──────┘
txt        └──────────┘└─────┘   └──────┘
par        └──────────┘└─────┘   └──────┘
pid                 └────────┘   └───────┘
st   ────────────────┘└─────────────────┘└┘
579        any_goals { change pos 1 with 1 },
id                            └─┘
src        └──────────┘└─────┘└─┘└────────┘
typ        └──────────┘└─────┘└─┘└────────┘
doc        └──────────┘└─────┘   └────────┘
txt        └──────────┘└─────┘   └────────┘
par        └──────────┘└─────┘   └────────┘
pid                 └────────┘   └─────────┘
st   ────────────────┘└───────────────────┘└┘
580        any_goals { change pos_num.bit0 with pos_num.bit ff },
id                            └──────────┘      └─────────┘ └┘
src        └──────────┘└─────┘└──────────┘└────┘└─────────┘└┘
typ        └──────────┘└─────┘└──────────┘└────┘└─────────┘└┘
doc        └──────────┘└─────┘            └────┘             
txt        └──────────┘└─────┘            └────┘             
par        └──────────┘└─────┘            └────┘             
pid                 └────────┘            └────┘             └┘
st   ────────────────┘└─────────────────────────────────────────┘
581        any_goals { change pos_num.bit1 with pos_num.bit tt },
id                            └──────────┘      └─────────┘ └┘
src        └──────────┘└─────┘└──────────┘└────┘└─────────┘└┘
typ        └──────────┘└─────┘└──────────┘└────┘└─────────┘└┘
doc        └──────────┘└─────┘            └────┘             
txt        └──────────┘└─────┘            └────┘             
par        └──────────┘└─────┘            └────┘             
pid                 └────────┘            └────┘             └┘
st   ────────────────┘└─────────────────────────────────────────┘
582        any_goals { change ((1:num):ℕ) with nat.bit tt 0 },
id                                └─┘          └─────┘ └┘
src        └──────────┘└─────┘  └┘└─┘└┘ └─────┘└─────┘└┘└─┘
typ        └──────────┘└─────┘  └┘└─┘└┘ └─────┘└─────┘└┘└─┘
doc        └──────────┘└─────┘  └┘└─┘└┘ └─────┘         └─┘
txt        └──────────┘└─────┘  └┘   └┘ └─────┘         └─┘
par        └──────────┘└─────┘  └┘   └┘ └─────┘         └─┘
pid                 └────────┘  └┘   └┘ └─────┘         └──┘
st   ────────────────┘└────────────────────────────────────┘└┘
583        all_goals {
src        └───────────
typ        └───────────
doc        └───────────
txt        └───────────
par        └───────────
pid                 └──
st   ────────────────┘
584          repeat {
src  ───────┘└────────
typ  ─────────────────
doc  ───────┘└────────
txt  ───────┘└────────
par  ─────────────────
pid  ─────────────────
st   ─────────────────
585            rw show ∀ b n, (pos (pos_num.bit b n) : ℕ) = nat.bit b ↑n,
id                             └─┘  └─────────┘             └─────┘
src  ─────────┘└─┘     └──┘  └─┘ └─────────┘  └──┘ └┘ └─────┘   └─
typ  ─────────┘└─┘     └──┘  └─┘ └─────────┘  └──┘ └┘ └─────┘   └─
doc  ─────────┘└─┘     └──┘                   └──┘ └┘           └─
txt  ─────────┘└─┘     └──┘                   └──┘ └┘           └─
par  ─────────┘└─┘     └──┘                   └──┘ └┘           └─
pid  ────────────┘     └──┘                   └──┘ └┘           └─
st   ─────────────────────────────────────────────────────────────────────
586               by intros; cases b; refl },
id                                 
src  ───────────────┘└────┘└┘└────┘ └┘└───┘└─
typ  ───────────────┘└────┘└┘└────┘└┘└───┘└──
doc  ───────────────┘└────┘└┘└────┘ └┘└───┘└─
txt  ───────────────┘└────┘└┘└────┘ └┘└───┘└─
par  ───────────────┘└────┘└┘└────┘ └┘└───┘└──
pid  ─────────────────────────────┘ └─────────
st   ──────────────┘└─────────────────────┘└─
587          rw nat.bitwise_bit },
id              └─────────────┘
src  ───────┘└─┘└─────────────┘
typ  ───────┘└─┘└─────────────┘
doc  ───────┘└─┘               
txt  ───────┘└─┘               
par  ───────┘└─┘               
pid  ──────────┘               └┘
st   ──────────────────────────┘└┘
588        any_goals { assumption },
src        └──────────┘└─────────┘
typ        └──────────┘└─────────┘
doc        └──────────┘└─────────┘
txt        └──────────┘└─────────┘
par        └──────────┘└─────────┘
pid                 └─────────────┘
st   ────────────────┘└──────────┘└┘
589        any_goals { rw [nat.bitwise_zero, p11], cases g tt tt; refl },
id                         └──────────────┘  └─┘             └┘
src        └──────────┘└──┘└──────────────┘└┘   └┘└────┘   └┘└┘└───┘
typ        └──────────┘└──┘└──────────────┘└┘└─┘└┘└────┘  └┘└┘└───┘
doc        └──────────┘└──┘                └┘   └┘└────┘     └┘└───┘
txt        └──────────┘└──┘                └┘   └┘└────┘     └┘└───┘
par        └──────────┘└──┘                └┘   └┘└────┘     └┘└───┘
pid                 └─────┘                └┘   └───────┘     └──────┘
st   ────────────────┘└───────────────────┘└───┘└─────────────────────┘└┘
590        any_goals { rw [nat.bitwise_zero_left, this, ← bit_to_nat, p1b] },
id                         └───────────────────┘  └──┘    └────────┘  └─┘
src        └──────────┘└──┘└───────────────────┘└┘    └──┘└────────┘└┘   └┘
typ        └──────────┘└──┘└───────────────────┘└┘└──┘└──┘└────────┘└┘└─┘└┘
doc        └──────────┘└──┘                     └┘    └──┘          └┘   └┘
txt        └──────────┘└──┘                     └┘    └──┘          └┘   └┘
par        └──────────┘└──┘                     └┘    └──┘          └┘   └┘
pid                 └─────┘                     └┘    └──┘          └┘   └─┘
st   ────────────────┘└────────────────────────┘└────┘└────────────┘└───┘└┘
591        any_goals { rw [nat.bitwise_zero_right _ gff, this, ← bit_to_nat, pb1] },
id                         └────────────────────┘   └─┘  └──┘    └────────┘  └─┘
src        └──────────┘└──┘└────────────────────┘└─┘   └┘    └──┘└────────┘└┘   └┘
typ        └──────────┘└──┘└────────────────────┘└─┘└─┘└┘└──┘└──┘└────────┘└┘└─┘└┘
doc        └──────────┘└──┘                      └─┘   └┘    └──┘          └┘   └┘
txt        └──────────┘└──┘                      └─┘   └┘    └──┘          └┘   └┘
par        └──────────┘└──┘                      └─┘   └┘    └──┘          └┘   └┘
pid                 └─────┘                      └─┘   └┘    └──┘          └┘   └─┘
st   ────────────────┘└───────────────────────────────┘└────┘└────────────┘└───┘└┘
592        all_goals { rw [← show ∀ n, ↑(p m n) = nat.bitwise g ↑m ↑n, from IH],
id                                               └─────────┘             └┘
src        └──────────┘└────┘     └┘      └┘ └─────────┘     └─────┘  └─
typ        └──────────┘└────┘     └┘     └┘ └─────────┘   └─────┘└┘└─
doc        └──────────┘└────┘     └┘      └┘                 └─────┘  └─
txt        └──────────┘└────┘     └┘      └┘                 └─────┘  └─
par        └──────────┘└────┘     └┘      └┘                 └─────┘  └─
pid                 └───────┘     └┘      └┘                 └─────┘  └──
st   ────────────────┘└──────────────────────────────────────────────────────┘└──
593          rw [← bit_to_nat, pbb] } }
id                 └────────┘  └─┘
src  ───────┘└────┘└────────┘└┘   └┘└┘
typ  ───────┘└────┘└────────┘└┘└─┘└┘└┘
doc  ───────┘└────┘          └┘   └┘└┘
txt  ───────┘└────┘          └┘   └┘└┘
par  ───────┘└────┘          └┘   └┘└┘
pid  ─────────────┘          └┘   └─┘
st   ───────────────────────┘└───┘└─
594    end
st   ────┘
595  
596    @[simp] theorem lor_to_nat   : ∀ m n, (lor    m n : ℕ) = nat.lor    m n :=
id                                          └─┘           └─────┘     
src                                           └─┘             └─────┘
typ                                         └─┘           └─────┘     
doc      └──┘
597    by apply bitwise_to_nat (λx y, pos (pos_num.lor x y)); intros; try {cases a}; try {cases b}; refl
id              └────────────┘        └─┘  └─────────┘                                         
src       └────┘└────────────┘  └───┘└─┘ └─────────┘  └┘  └────┘  └───┘└────┘   └───┘└────┘   └────
typ       └────┘└────────────┘  └───┘└─┘ └─────────┘  └┘  └────┘  └───┘└────┘  └───┘└────┘  └────
doc       └────┘                └───┘                 └┘  └────┘  └───┘└────┘   └───┘└────┘   └────
txt       └────┘                └───┘                 └┘  └────┘  └───┘└────┘   └───┘└────┘   └────
par       └────┘                └───┘                 └┘  └────┘  └───┘└────┘   └───┘└────┘   └────
pid                            └───┘                 └┘             └──────┘      └──────┘       
st       └────────────────────────────────────────────────────────────────┘└─────┘└┘└────┘└─────┘└┘└─────
598    @[simp] theorem land_to_nat  : ∀ m n, (land   m n : ℕ) = nat.land   m n :=
id                                          └──┘          └──────┘    
src  ─┘                                       └──┘            └──────┘
typ  ─┘                                     └──┘          └──────┘    
doc  ─┘  └──┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
599    by apply bitwise_to_nat pos_num.land; intros; try {cases a}; try {cases b}; refl
id              └────────────┘ └──────────┘                                   
src       └────┘└────────────┘└──────────┘  └────┘  └───┘└────┘   └───┘└────┘   └────
typ       └────┘└────────────┘└──────────┘  └────┘  └───┘└────┘  └───┘└────┘  └────
doc       └────┘                            └────┘  └───┘└────┘   └───┘└────┘   └────
txt       └────┘                            └────┘  └───┘└────┘   └───┘└────┘   └────
par       └────┘                            └────┘  └───┘└────┘   └───┘└────┘   └────
pid                                                   └──────┘      └──────┘       
st       └───────────────────────────────────────────────┘└─────┘└┘└────┘└─────┘└┘└─────
600    @[simp] theorem ldiff_to_nat : ∀ m n, (ldiff  m n : ℕ) = nat.ldiff  m n :=
id                                          └───┘         └───────┘   
src  ─┘                                       └───┘           └───────┘
typ  ─┘                                     └───┘         └───────┘   
doc  ─┘  └──┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
601    by apply bitwise_to_nat pos_num.ldiff; intros; try {cases a}; try {cases b}; refl
id              └────────────┘ └───────────┘                                   
src       └────┘└────────────┘└───────────┘  └────┘  └───┘└────┘   └───┘└────┘   └────
typ       └────┘└────────────┘└───────────┘  └────┘  └───┘└────┘  └───┘└────┘  └────
doc       └────┘                             └────┘  └───┘└────┘   └───┘└────┘   └────
txt       └────┘                             └────┘  └───┘└────┘   └───┘└────┘   └────
par       └────┘                             └────┘  └───┘└────┘   └───┘└────┘   └────
pid                                                    └──────┘      └──────┘       
st       └────────────────────────────────────────────────┘└─────┘└┘└────┘└─────┘└┘└─────
602    @[simp] theorem lxor_to_nat  : ∀ m n, (lxor   m n : ℕ) = nat.lxor   m n :=
id                                          └──┘          └──────┘    
src  ─┘                                       └──┘            └──────┘
typ  ─┘                                     └──┘          └──────┘    
doc  ─┘  └──┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
603    by apply bitwise_to_nat pos_num.lxor; intros; try {cases a}; try {cases b}; refl
id              └────────────┘ └──────────┘                                   
src       └────┘└────────────┘└──────────┘  └────┘  └───┘└────┘   └───┘└────┘   └────
typ       └────┘└────────────┘└──────────┘  └────┘  └───┘└────┘  └───┘└────┘  └────
doc       └────┘                            └────┘  └───┘└────┘   └───┘└────┘   └────
txt       └────┘                            └────┘  └───┘└────┘   └───┘└────┘   └────
par       └────┘                            └────┘  └───┘└────┘   └───┘└────┘   └────
pid                                                   └──────┘      └──────┘       
st       └───────────────────────────────────────────────┘└─────┘└┘└────┘└─────┘└┘└─────
604  
src  
typ  
doc  
txt  
par  
pid  
st   
605    @[simp] theorem shiftl_to_nat (m n) : (shiftl m n : ℕ) = nat.shiftl m n :=
id                                           └────┘        └────────┘  
src  ─┘                                      └────┘          └────────┘
typ  ─┘                                      └────┘        └────────┘  
doc  ─┘  └──┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
606    begin
st     └─────
607      cases m; dunfold shiftl, {symmetry, apply nat.zero_shiftl},
id                                                └─────────────┘
src      └────┘   └────────────┘   └──────┘  └────┘└─────────────┘
typ      └────┘  └────────────┘   └──────┘  └────┘└─────────────┘
doc      └────┘   └────────────┘   └──────┘  └────┘
txt      └────┘   └────────────┘   └──────┘  └────┘
par      └────┘   └────────────┘   └──────┘  └────┘
pid                     └─────┘                  
st   ──────────────────────────┘└─────────┘└─────────────────────┘└┘
608      simp, induction n with n IH, {refl},
id                       
src      └──┘  └────────┘ └────────┘   └──┘
typ      └──┘  └────────┘└────────┘   └──┘
doc      └──┘  └────────┘ └────────┘   └──┘
txt      └──┘  └────────┘ └────────┘   └──┘
par      └──┘  └────────┘ └────────┘   └──┘
pid                      └───────┘
st   ───────┘└─────────────────────┘└─────┘└┘
609      simp [pos_num.shiftl, nat.shiftl_succ], rw ←IH
id             └────────────┘  └─────────────┘       └┘
src      └────┘└────────────┘└┘└─────────────┘  └──┘  
typ      └────┘└────────────┘└┘└─────────────┘  └──┘└┘
doc      └────┘              └┘                 └──┘  
txt      └────┘              └┘                 └──┘  
par      └────┘              └┘                 └──┘  
pid                        └┘                   └┘  
st   ─────────────────────────────────────────┘└────────
610    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
611  
612    @[simp] theorem shiftr_to_nat (m n) : (shiftr m n : ℕ) = nat.shiftr m n :=
id                                            └────┘        └────────┘  
src                                           └────┘          └────────┘
typ                                           └────┘        └────────┘  
doc      └──┘
613    begin
st     └─────
614      cases m with m; dunfold shiftr, {symmetry, apply nat.zero_shiftr},
id                                                       └─────────────┘
src      └────┘ └─────┘  └────────────┘   └──────┘  └────┘└─────────────┘
typ      └────┘└─────┘  └────────────┘   └──────┘  └────┘└─────────────┘
doc      └────┘ └─────┘  └────────────┘   └──────┘  └────┘
txt      └────┘ └─────┘  └────────────┘   └──────┘  └────┘
par      └────┘ └─────┘  └────────────┘   └──────┘  └────┘
pid            └─────┘         └─────┘                  
st   ─────────────────────────────────┘└─────────┘└─────────────────────┘└┘
615      induction n with n IH generalizing m, {cases m; refl},
id                                                   
src      └────────┘ └───────────────────────┘   └────┘   └──┘
typ      └────────┘└───────────────────────┘   └────┘  └──┘
doc      └────────┘ └───────────────────────┘   └────┘   └──┘
txt      └────────┘ └───────────────────────┘   └────┘   └──┘
par      └────────┘ └───────────────────────┘   └────┘   └──┘
pid                └───────┘└─────────────┘        
st   ───────────────────────────────────────┘└──────────────┘└┘
616      cases m with m m; dunfold pos_num.shiftr,
id             
src      └────┘ └───────┘  └────────────────────┘
typ      └────┘└───────┘  └────────────────────┘
doc      └────┘ └───────┘  └────────────────────┘
txt      └────┘ └───────┘  └────────────────────┘
par      └────┘ └───────┘  └────────────────────┘
pid            └───────┘         └─────────────┘
st   ───────────────────────────────────────────┘└─
617      { rw [nat.shiftr_eq_div_pow], symmetry, apply nat.div_eq_of_lt,
id             └───────────────────┘                   └──────────────┘
src        └──┘└───────────────────┘  └──────┘  └────┘└──────────────┘
typ        └──┘└───────────────────┘  └──────┘  └────┘└──────────────┘
doc        └──┘                       └──────┘  └────┘
txt        └──┘                       └──────┘  └────┘
par        └──┘                       └──────┘  └────┘
pid          └┘                                      
st   ─────┘└───────────────────────┘└─────────┘└──────────────────────┘└─
618        exact @nat.pow_lt_pow_of_lt_right 2 dec_trivial 0 (n+1) (nat.succ_pos _) },
id                └────────────────────────┘   └─────────┘        └──────────┘
src        └────┘ └────────────────────────┘└─┘└─────────┘└─┘  └─┘ └──────────┘└──┘
typ        └────┘ └────────────────────────┘└─┘└─────────┘└─┘ └─┘ └──────────┘└──┘
doc        └────┘                           └─┘└─────────┘└─┘   └─┘             └──┘
txt        └────┘                           └─┘           └─┘   └─┘             └──┘
par        └────┘                           └─┘           └─┘   └─┘             └──┘
pid                                        └─┘           └─┘   └─┘             └─┘
st   ──────────────────────────────────────────────────────────────────────────────┘└┘
619      { transitivity, apply IH,
src        └──────────┘  └────┘
typ        └──────────┘  └────┘
doc        └──────────┘  └────┘
txt        └──────────┘  └────┘
par        └──────────┘  └────┘
pid                           
st   ─────┘└──────────┘└────────┘└─
620        change nat.shiftr m n = nat.shiftr (bit1 m) (n+1),
id                                └────────┘  └──┘    
src        └─────┘            └────────┘ └──┘ └┘   └┘
typ        └─────┘            └────────┘ └──┘└┘  └┘
doc        └─────┘                             └┘   └┘
txt        └─────┘                             └┘   └┘
par        └─────┘                             └┘   └┘
pid                                           └┘   └┘
st   ──────────────────────────────────────────────────────┘└─
621        rw [add_comm n 1, nat.shiftr_add],
id             └──────┘     └────────────┘
src        └──┘└──────┘ └──┘└────────────┘
typ        └──┘└──────┘└──┘└────────────┘
doc        └──┘         └──┘              
txt        └──┘         └──┘              
par        └──┘         └──┘              
pid          └┘         └──┘              
st   ────────────────────┘└───────────────┘└──
622        apply congr_arg (λx, nat.shiftr x n), unfold nat.shiftr,
id               └───────┘      └────────┘   
src        └────┘└───────┘  └─┘└────────┘    └───────────────┘
typ        └────┘└───────┘  └─┘└────────┘   └───────────────┘
doc        └────┘           └─┘              └───────────────┘
txt        └────┘           └─┘              └───────────────┘
par        └────┘           └─┘              └───────────────┘
pid                        └─┘                    └─────────┘
st   ─────────────────────────────────────────┘└─────────────────┘└─
623        change (bit1 ↑m : ℕ) with nat.bit tt m,
id                 └──┘            └─────┘ └┘ 
src        └─────┘ └──┘ └─┘ └─────┘└─────┘└┘
typ        └─────┘ └──┘└─┘ └─────┘└─────┘└┘
doc        └─────┘       └─┘ └─────┘         
txt        └─────┘       └─┘ └─────┘         
par        └─────┘       └─┘ └─────┘         
pid                     └─┘ └────┘         
st   ───────────────────────────────────────────┘└─
624        rw nat.div2_bit },
id            └──────────┘
src        └─┘└──────────┘
typ        └─┘└──────────┘
doc        └─┘            
txt        └─┘            
par        └─┘            
pid                      
st   ─────────────────────┘└┘
625      { transitivity, apply IH,
src        └──────────┘  └────┘
typ        └──────────┘  └────┘
doc        └──────────┘  └────┘
txt        └──────────┘  └────┘
par        └──────────┘  └────┘
pid                           
st   ─────────────────┘└────────┘└─
626        change nat.shiftr m n = nat.shiftr (bit0 m) (n + 1),
id                                 └────────┘  └──┘    
src        └─────┘             └────────┘ └──┘ └┘   └─┘
typ        └─────┘             └────────┘ └──┘└┘  └─┘
doc        └─────┘                             └┘   └─┘
txt        └─────┘                             └┘   └─┘
par        └─────┘                             └┘   └─┘
pid                                           └┘   └─┘
st   ────────────────────────────────────────────────────────┘└─
627        rw [add_comm n 1, nat.shiftr_add],
id             └──────┘     └────────────┘
src        └──┘└──────┘ └──┘└────────────┘
typ        └──┘└──────┘└──┘└────────────┘
doc        └──┘         └──┘              
txt        └──┘         └──┘              
par        └──┘         └──┘              
pid          └┘         └──┘              
st   ────────────────────┘└───────────────┘└──
628        apply congr_arg (λx, nat.shiftr x n), unfold nat.shiftr,
id               └───────┘      └────────┘   
src        └────┘└───────┘  └─┘└────────┘    └───────────────┘
typ        └────┘└───────┘  └─┘└────────┘   └───────────────┘
doc        └────┘           └─┘              └───────────────┘
txt        └────┘           └─┘              └───────────────┘
par        └────┘           └─┘              └───────────────┘
pid                        └─┘                    └─────────┘
st   ─────────────────────────────────────────┘└─────────────────┘└─
629        change (bit0 ↑m : ℕ) with nat.bit ff m,
id                 └──┘             └─────┘ └┘ 
src        └─────┘ └──┘  └─┘ └─────┘└─────┘└┘
typ        └─────┘ └──┘ └─┘ └─────┘└─────┘└┘
doc        └─────┘       └─┘ └─────┘         
txt        └─────┘       └─┘ └─────┘         
par        └─────┘       └─┘ └─────┘         
pid                     └─┘ └────┘         
st   ───────────────────────────────────────────┘└─
630        rw nat.div2_bit }
id            └──────────┘
src        └─┘└──────────┘
typ        └─┘└──────────┘
doc        └─┘            
txt        └─┘            
par        └─┘            
pid                      
st   ─────────────────────┘└─
631    end
st   ────┘
632  
633    @[simp] theorem test_bit_to_nat (m n) : test_bit m n = nat.test_bit m n :=
id                                             └──────┘    └──────────┘  
src                                            └──────┘      └──────────┘
typ                                            └──────┘    └──────────┘  
doc      └──┘
634    begin
st     └─────
635      cases m with m; unfold test_bit nat.test_bit,
id             
src      └────┘ └─────┘  └──────────────────────────┘
typ      └────┘└─────┘  └──────────────────────────┘
doc      └────┘ └─────┘  └──────────────────────────┘
txt      └────┘ └─────┘  └──────────────────────────┘
par      └────┘ └─────┘  └──────────────────────────┘
pid            └─────┘        └────────────────────┘
st   ───────────────────────────────────────────────┘└─
636      { change (zero : nat) with 0, rw nat.zero_shiftr, refl },
id                 └──┘   └─┘             └─────────────┘
src        └─────┘ └──┘└─┘└─┘└──────┘  └─┘└─────────────┘  └───┘
typ        └─────┘ └──┘└─┘└─┘└──────┘  └─┘└─────────────┘  └───┘
doc        └─────┘     └─┘   └──────┘  └─┘                 └───┘
txt        └─────┘     └─┘   └──────┘  └─┘                 └───┘
par        └─────┘     └─┘   └──────┘  └─┘                 └───┘
pid                   └─┘   └────┘                         
st   ─────┘└────────────────────────┘└──────────────────┘└─────┘└┘
637      induction n with n IH generalizing m;
id                 
src      └────────┘ └───────────────────────┘
typ      └────────┘└───────────────────────┘
doc      └────────┘ └───────────────────────┘
txt      └────────┘ └───────────────────────┘
par      └────────┘ └───────────────────────┘
pid                └───────┘└─────────────┘
st   ──────────────────────────────────────────
638      cases m; dunfold pos_num.test_bit, {refl},
id             
src      └────┘   └──────────────────────┘   └──┘
typ      └────┘  └──────────────────────┘   └──┘
doc      └────┘   └──────────────────────┘   └──┘
txt      └────┘   └──────────────────────┘   └──┘
par      └────┘   └──────────────────────┘   └──┘
pid                     └───────────────┘
st   ────────────────────────────────────┘└─────┘└┘
639      { exact (nat.bodd_bit _ _).symm },
id                └──────────┘
src        └────┘ └──────────┘└─────────┘
typ        └────┘ └──────────┘└─────────┘
doc        └────┘             └─────────┘
txt        └────┘             └─────────┘
par        └────┘             └─────────┘
pid                          └───────┘└┘
st   ─────┘└────────────────────────────┘└┘
640      { exact (nat.bodd_bit _ _).symm },
id                └──────────┘
src        └────┘ └──────────┘└─────────┘
typ        └────┘ └──────────┘└─────────┘
doc        └────┘             └─────────┘
txt        └────┘             └─────────┘
par        └────┘             └─────────┘
pid                          └───────┘└┘
st   ─────┘└────────────────────────────┘└┘
641      { change ff = nat.bodd (nat.shiftr 1 (n + 1)),
id                └┘  └──────┘  └────────┘     
src        └─────┘└┘└──────┘ └────────┘└─┘  └──┘
typ        └─────┘└┘└──────┘ └────────┘└─┘ └──┘
doc        └─────┘                      └─┘   └──┘
txt        └─────┘                      └─┘   └──┘
par        └─────┘                      └─┘   └──┘
pid                                    └─┘   └──┘
st   ─────┘└─────────────────────────────────────────┘└─
642        rw [add_comm, nat.shiftr_add], change nat.shiftr 1 1 with 0,
id             └──────┘  └────────────┘          └────────┘
src        └──┘└──────┘└┘└────────────┘  └─────┘└────────┘└─────────┘
typ        └──┘└──────┘└┘└────────────┘  └─────┘└────────┘└─────────┘
doc        └──┘        └┘                └─────┘          └─────────┘
txt        └──┘        └┘                └─────┘          └─────────┘
par        └──┘        └┘                └─────┘          └─────────┘
pid          └┘        └┘                                └─┘└─────┘
st   ─────────────────┘└──────────────┘└─────────────────────────────┘└─
643        rw nat.zero_shiftr; refl },
id            └─────────────┘
src        └─┘└─────────────┘  └───┘
typ        └─┘└─────────────┘  └───┘
doc        └─┘                 └───┘
txt        └─┘                 └───┘
par        └─┘                 └───┘
pid                               
st   ──────────────────────────────┘└┘
644      { change pos_num.test_bit m n = nat.bodd (nat.shiftr (nat.bit tt m) (n + 1)),
id                └──────────────┘       └──────┘  └────────┘  └─────┘ └┘    
src        └─────┘└──────────────┘   └──────┘ └────────┘ └─────┘└┘ └┘   └──┘
typ        └─────┘└──────────────┘   └──────┘ └────────┘ └─────┘└┘└┘  └──┘
doc        └─────┘                                                 └┘   └──┘
txt        └─────┘                                                 └┘   └──┘
par        └─────┘                                                 └┘   └──┘
pid                                                               └┘   └──┘
st   ─────┘└────────────────────────────────────────────────────────────────────────┘└─
645        rw [add_comm, nat.shiftr_add], unfold nat.shiftr,
id             └──────┘  └────────────┘
src        └──┘└──────┘└┘└────────────┘  └───────────────┘
typ        └──┘└──────┘└┘└────────────┘  └───────────────┘
doc        └──┘        └┘                └───────────────┘
txt        └──┘        └┘                └───────────────┘
par        └──┘        └┘                └───────────────┘
pid          └┘        └┘                      └─────────┘
st   ─────────────────┘└──────────────┘└──────────────────┘└─
646        rw nat.div2_bit, apply IH },
id            └──────────┘
src        └─┘└──────────┘  └────┘  
typ        └─┘└──────────┘  └────┘  
doc        └─┘              └────┘  
txt        └─┘              └────┘  
par        └─┘              └────┘  
pid                               
st   ────────────────────┘└─────────┘└┘
647      { change pos_num.test_bit m n = nat.bodd (nat.shiftr (nat.bit ff m) (n + 1)),
id                └──────────────┘       └──────┘  └────────┘  └─────┘ └┘    
src        └─────┘└──────────────┘   └──────┘ └────────┘ └─────┘└┘ └┘   └──┘
typ        └─────┘└──────────────┘   └──────┘ └────────┘ └─────┘└┘└┘  └──┘
doc        └─────┘                                                 └┘   └──┘
txt        └─────┘                                                 └┘   └──┘
par        └─────┘                                                 └┘   └──┘
pid                                                               └┘   └──┘
st   ───────────────────────────────────────────────────────────────────────────────┘└─
648        rw [add_comm, nat.shiftr_add], unfold nat.shiftr,
id             └──────┘  └────────────┘
src        └──┘└──────┘└┘└────────────┘  └───────────────┘
typ        └──┘└──────┘└┘└────────────┘  └───────────────┘
doc        └──┘        └┘                └───────────────┘
txt        └──┘        └┘                └───────────────┘
par        └──┘        └┘                └───────────────┘
pid          └┘        └┘                      └─────────┘
st   ─────────────────┘└──────────────┘└──────────────────┘└─
649        rw nat.div2_bit, apply IH },
id            └──────────┘
src        └─┘└──────────┘  └────┘  
typ        └─┘└──────────┘  └────┘  
doc        └─┘              └────┘  
txt        └─┘              └────┘  
par        └─┘              └────┘  
pid                               
st   ────────────────────┘└─────────┘└──
650    end
st   ────┘
651  
652  end num
653  
654  namespace znum
655    variables {α : Type*}
656    open pos_num
657  
658    @[simp] theorem cast_zero [has_zero α] [has_one α] [has_add α] [has_neg α] :
id                                └──────┘    └─────┘    └─────┘    └─────┘ 
src                               └──────┘     └─────┘     └─────┘     └─────┘
typ                               └──────┘    └─────┘    └─────┘    └─────┘ 
doc      └──┘
659      ((0 : znum) : α) = 0 := rfl
id             └──┘            └─┘
src            └──┘             └─┘
typ            └──┘            └─┘
doc            └──┘
660  
661    @[simp] theorem cast_zero' [has_zero α] [has_one α] [has_add α] [has_neg α] :
id                                 └──────┘    └─────┘    └─────┘    └─────┘ 
src                                └──────┘     └─────┘     └─────┘     └─────┘
typ                                └──────┘    └─────┘    └─────┘    └─────┘ 
doc      └──┘
662      (znum.zero : α) = 0 := rfl
id        └───────┘           └─┘
src       └───────┘            └─┘
typ       └───────┘           └─┘
663  
664    @[simp] theorem cast_one [has_zero α] [has_one α] [has_add α] [has_neg α] :
id                               └──────┘    └─────┘    └─────┘    └─────┘ 
src                              └──────┘     └─────┘     └─────┘     └─────┘
typ                              └──────┘    └─────┘    └─────┘    └─────┘ 
doc      └──┘
665      ((1 : znum) : α) = 1 := rfl
id             └──┘            └─┘
src            └──┘             └─┘
typ            └──┘            └─┘
doc            └──┘
666  
667    @[simp] theorem cast_pos [has_zero α] [has_one α] [has_add α] [has_neg α]
id                               └──────┘    └─────┘    └─────┘    └─────┘ 
src                              └──────┘     └─────┘     └─────┘     └─────┘
typ                              └──────┘    └─────┘    └─────┘    └─────┘ 
doc      └──┘
668      (n : pos_num) : (pos n : α) = n := rfl
id            └─────┘     └─┘           └─┘
src           └─────┘     └─┘              └─┘
typ           └─────┘     └─┘           └─┘
doc           └─────┘
669  
670    @[simp] theorem cast_neg [has_zero α] [has_one α] [has_add α] [has_neg α]
id                               └──────┘    └─────┘    └─────┘    └─────┘ 
src                              └──────┘     └─────┘     └─────┘     └─────┘
typ                              └──────┘    └─────┘    └─────┘    └─────┘ 
doc      └──┘
671      (n : pos_num) : (neg n : α) = -n := rfl
id            └─────┘     └─┘           └─┘
src           └─────┘     └─┘              └─┘
typ           └─────┘     └─┘           └─┘
doc           └─────┘
672  
673    @[simp] theorem cast_zneg [add_group α] [has_one α] : ∀ n, ((-n : znum) : α) = -n
id                                └───────┘    └─────┘              └──┘       
src                               └───────┘     └─────┘                 └──┘        
typ                               └───────┘    └─────┘              └──┘       
doc      └──┘                                                            └──┘
674    | 0       := neg_zero.symm
id                  └──────┘└───┘
src                 └──────┘└───┘
typ                 └──────┘└───┘
675    | (pos p) := rfl
id        └─┘       └─┘
src       └─┘       └─┘
typ       └─┘       └─┘
676    | (neg p) := (neg_neg _).symm
id        └─┘        └─────┘   └──┘
src       └─┘        └─────┘   └──┘
typ       └─┘        └─────┘   └──┘
677  
678    theorem neg_zero : (-0 : znum) = 0 := rfl
id                             └──┘        └─┘
src                            └──┘        └─┘
typ                            └──┘        └─┘
doc                             └──┘
679    theorem zneg_pos (n : pos_num) : -pos n = neg n := rfl
id                           └─────┘    └─┘   └─┘     └─┘
src                          └─────┘    └─┘    └─┘      └─┘
typ                          └─────┘    └─┘   └─┘     └─┘
doc                          └─────┘
680    theorem zneg_neg (n : pos_num) : -neg n = pos n := rfl
id                           └─────┘    └─┘   └─┘     └─┘
src                          └─────┘    └─┘    └─┘      └─┘
typ                          └─────┘    └─┘   └─┘     └─┘
doc                          └─────┘
681    theorem zneg_zneg (n : znum) : - -n = n := by cases n; refl
id                            └──┘                    
src                           └──┘                └────┘   └────
typ                           └──┘              └────┘  └────
doc                           └──┘                   └────┘   └────
txt                                                  └────┘   └────
par                                                  └────┘   └────
pid                                                              
st                                                  └──────────────
682    theorem zneg_bit1 (n : znum) : -n.bit1 = (-n).bitm1 := by cases n; refl
id                            └──┘    └───┘    └───┘              
src  ─┘                       └──┘     └───┘     └───┘        └────┘   └────
typ  ─┘                       └──┘    └───┘    └───┘        └────┘  └────
doc  ─┘                       └──┘                               └────┘   └────
txt  ─┘                                                          └────┘   └────
par  ─┘                                                          └────┘   └────
pid  ─┘                                                                      
st   ─┘                                                         └──────────────
683    theorem zneg_bitm1 (n : znum) : -n.bitm1 = (-n).bit1 := by cases n; refl
id                             └──┘    └────┘    └──┘              
src  ─┘                        └──┘     └────┘     └──┘        └────┘   └────
typ  ─┘                        └──┘    └────┘    └──┘        └────┘  └────
doc  ─┘                        └──┘                               └────┘   └────
txt  ─┘                                                           └────┘   └────
par  ─┘                                                           └────┘   └────
pid  ─┘                                                                       
st   ─┘                                                          └──────────────
684  
src  
typ  
doc  
txt  
par  
pid  
st   
685    theorem zneg_succ (n : znum) : -n.succ = (-n).pred :=
id                            └──┘    └───┘    └──┘
src  ─┘                       └──┘     └───┘     └──┘
typ  ─┘                       └──┘    └───┘    └──┘
doc  ─┘                       └──┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
686    by cases n; try {refl}; rw [succ, num.zneg_to_znum_neg]; refl
id                                └──┘  └──────────────────┘
src       └────┘   └───┘└──┘  └──┘└──┘└┘└──────────────────┘  └────
typ       └────┘  └───┘└──┘  └──┘└──┘└┘└──────────────────┘  └────
doc       └────┘   └───┘└──┘  └──┘    └┘                      └────
txt       └────┘   └───┘└──┘  └──┘    └┘                      └────
par       └────┘   └───┘└──┘  └──┘    └┘                      └────
pid                  └─────┘    └┘    └┘                          
st       └─────────────┘└──┘└┘└───┘└──┘└────────────────────┘└──────
687  
src  
typ  
doc  
txt  
par  
pid  
st   
688    theorem zneg_pred (n : znum) : -n.pred = (-n).succ :=
id                            └──┘    └───┘    └──┘
src  ─┘                       └──┘     └───┘     └──┘
typ  ─┘                       └──┘    └───┘    └──┘
doc  ─┘                       └──┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
689    by rw [← zneg_zneg (succ (-n)), zneg_succ, zneg_zneg]
id              └───────┘  └──┘      └───────┘  └───────┘
src       └────┘└───────┘ └──┘  └──┘└───────┘└┘└───────┘└─
typ       └────┘└───────┘ └──┘ └──┘└───────┘└┘└───────┘└─
doc       └────┘                 └──┘         └┘         └─
txt       └────┘                 └──┘         └┘         └─
par       └────┘                 └──┘         └┘         └─
pid         └──┘                 └──┘         └┘         
st       └──────────────────────────┘└─────────┘└─────────┘
690  
src  
typ  
doc  
txt  
par  
pid  
st   
691    @[simp] theorem neg_of_int : ∀ n, ((-n : ℤ) : znum) = -n
id                                               └──┘   
src  ─┘                                            └──┘   
typ  ─┘                                          └──┘   
doc  ─┘  └──┘                                        └──┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
692    | (n+1:ℕ) := rfl
id                └─┘
src               └─┘
typ               └─┘
693    | 0       := rfl
id                  └─┘
src                 └─┘
typ                 └─┘
694    | -[1+n]  := (zneg_zneg _).symm
id       └──┘       └───────┘   └──┘
src      └──┘       └───────┘   └──┘
typ      └──┘       └───────┘   └──┘
695  
696    @[simp] theorem abs_to_nat : ∀ n, (abs n : ℕ) = int.nat_abs n
id                                       └─┘       └─────────┘ 
src                                       └─┘        └─────────┘
typ                                      └─┘       └─────────┘ 
doc      └──┘
697    | 0       := rfl
id                  └─┘
src                 └─┘
typ                 └─┘
698    | (pos p) := congr_arg int.nat_abs p.to_nat_to_int
id        └─┘      └───────┘ └─────────┘  └────────────┘
src       └─┘       └───────┘ └─────────┘  └────────────┘
typ       └─┘      └───────┘ └─────────┘  └────────────┘
699    | (neg p) := show int.nat_abs ((p:ℕ):ℤ) = int.nat_abs (- p),
id        └─┘           └─────────┘          └─────────┘  
src       └─┘            └─────────┘          └─────────┘  
typ       └─┘           └─────────┘          └─────────┘  
700      by rw [p.to_nat_to_int, int.nat_abs_neg]
id                               └─────────────┘
src         └──┘               └┘└─────────────┘└─
typ         └──┘└─────────────┘└┘└─────────────┘└─
doc         └──┘               └┘               └─
txt         └──┘               └┘               └─
par         └──┘               └┘               └─
pid           └┘               └┘               
st         └──────────────────┘└───────────────┘
701  
src  
typ  
doc  
txt  
par  
pid  
st   
702    @[simp] theorem abs_to_znum : ∀ n : num, abs n.to_znum = n
id                                        └─┘  └─┘ └──────┘  
src  ─┘                                    └─┘  └─┘  └──────┘ 
typ  ─┘                                   └─┘  └─┘ └──────┘  
doc  ─┘  └──┘                              └─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
703    | 0           := rfl
id                      └─┘
src                     └─┘
typ                     └─┘
704    | (num.pos p) := rfl
id        └─────┘       └─┘
src       └─────┘       └─┘
typ       └─────┘       └─┘
705  
706    @[simp] theorem cast_to_int [add_group α] [has_one α] : ∀ n : znum, ((n : ℤ) : α) = n
id                                  └───────┘    └─────┘          └──┘              
src                                 └───────┘     └─────┘            └──┘               
typ                                 └───────┘    └─────┘          └──┘              
doc      └──┘                                                        └──┘
707    | 0       := rfl
id                  └─┘
src                 └─┘
typ                 └─┘
708    | (pos p) := by rw [cast_pos, cast_pos, pos_num.cast_to_int]
id        └─┘              └──────┘  └──────┘  └─────────────────┘
src       └─┘          └──┘└──────┘└┘└──────┘└┘└─────────────────┘└─
typ       └─┘          └──┘└──────┘└┘└──────┘└┘└─────────────────┘└─
doc                    └──┘        └┘        └┘                   └─
txt                    └──┘        └┘        └┘                   └─
par                    └──┘        └┘        └┘                   └─
pid                      └┘        └┘        └┘                   
st                    └───────────┘└────────┘└───────────────────┘
709    | (neg p) := by rw [cast_neg, cast_neg, int.cast_neg, pos_num.cast_to_int]
id        └─┘              └──────┘  └──────┘  └──────────┘  └─────────────────┘
src  ─┘   └─┘          └──┘└──────┘└┘└──────┘└┘└──────────┘└┘└─────────────────┘└─
typ  ─┘   └─┘          └──┘└──────┘└┘└──────┘└┘└──────────┘└┘└─────────────────┘└─
doc  ─┘                └──┘        └┘        └┘            └┘                   └─
txt  ─┘                └──┘        └┘        └┘            └┘                   └─
par  ─┘                └──┘        └┘        └┘            └┘                   └─
pid  ─┘                  └┘        └┘        └┘            └┘                   
st   ─┘               └───────────┘└────────┘└────────────┘└───────────────────┘
710  
src  
typ  
doc  
txt  
par  
pid  
st   
711    theorem bit0_of_bit0 : ∀ n : znum, _root_.bit0 n = n.bit0
id                                 └──┘  └─────────┘   └───┘
src  ─┘                             └──┘  └─────────┘     └───┘
typ  ─┘                            └──┘  └─────────┘   └───┘
doc  ─┘                             └──┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
712    | 0       := rfl
id                  └─┘
src                 └─┘
typ                 └─┘
713    | (pos a) := congr_arg pos a.bit0_of_bit0
id        └─┘      └───────┘ └─┘  └───────────┘
src       └─┘       └───────┘ └─┘  └───────────┘
typ       └─┘      └───────┘ └─┘  └───────────┘
714    | (neg a) := congr_arg neg a.bit0_of_bit0
id        └─┘      └───────┘ └─┘  └───────────┘
src       └─┘       └───────┘ └─┘  └───────────┘
typ       └─┘      └───────┘ └─┘  └───────────┘
715  
716    theorem bit1_of_bit1 : ∀ n : znum, _root_.bit1 n = n.bit1
id                                 └──┘  └─────────┘   └───┘
src                                 └──┘  └─────────┘     └───┘
typ                                └──┘  └─────────┘   └───┘
doc                                 └──┘
717    | 0       := rfl
id                  └─┘
src                 └─┘
typ                 └─┘
718    | (pos a) := congr_arg pos a.bit1_of_bit1
id        └─┘      └───────┘ └─┘  └───────────┘
src       └─┘       └───────┘ └─┘  └───────────┘
typ       └─┘      └───────┘ └─┘  └───────────┘
719    | (neg a) := show pos_num.sub' 1 (_root_.bit0 a) = _,
id        └─┘           └──────────┘    └─────────┘    
src       └─┘            └──────────┘    └─────────┘    
typ       └─┘           └──────────┘    └─────────┘    
720      by rw [pos_num.one_sub', a.bit0_of_bit0]; refl
id              └──────────────┘
src         └──┘└──────────────┘└┘                └────
typ         └──┘└──────────────┘└┘└────────────┘  └────
doc         └──┘                └┘                └────
txt         └──┘                └┘                └────
par         └──┘                └┘                └────
pid           └┘                └┘                    
st         └───────────────────┘└──────────────┘└──────
721  
src  
typ  
doc  
txt  
par  
pid  
st   
722    @[simp] theorem cast_bit0 [add_group α] [has_one α] :
id                                └───────┘    └─────┘ 
src  ─┘                           └───────┘     └─────┘
typ  ─┘                           └───────┘    └─────┘ 
doc  ─┘  └──┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
723      ∀ n : znum, (n.bit0 : α) = bit0 n
id            └──┘   └───┘      └──┘ 
src            └──┘    └───┘       └──┘
typ           └──┘   └───┘      └──┘ 
doc            └──┘
724    | 0       := (add_zero _).symm
id                   └──────┘   └──┘
src                  └──────┘   └──┘
typ                  └──────┘   └──┘
725    | (pos p) := by rw [znum.bit0, cast_pos, cast_pos]; refl
id        └─┘              └───────┘  └──────┘  └──────┘
src       └─┘          └──┘└───────┘└┘└──────┘└┘└──────┘  └────
typ       └─┘          └──┘└───────┘└┘└──────┘└┘└──────┘  └────
doc                    └──┘         └┘        └┘          └────
txt                    └──┘         └┘        └┘          └────
par                    └──┘         └┘        └┘          └────
pid                      └┘         └┘        └┘              
st                    └────────────┘└────────┘└────────┘└──────
726    | (neg p) := by rw [znum.bit0, cast_neg, cast_neg, pos_num.cast_bit0,
id        └─┘              └───────┘  └──────┘  └──────┘  └───────────────┘
src  ─┘   └─┘          └──┘└───────┘└┘└──────┘└┘└──────┘└┘└───────────────┘└─
typ  ─┘   └─┘          └──┘└───────┘└┘└──────┘└┘└──────┘└┘└───────────────┘└─
doc  ─┘                └──┘         └┘        └┘        └┘                 └─
txt  ─┘                └──┘         └┘        └┘        └┘                 └─
par  ─┘                └──┘         └┘        └┘        └┘                 └─
pid  ─┘                  └┘         └┘        └┘        └┘                 └─
st   ─┘               └────────────┘└────────┘└────────┘└─────────────────┘└─
727                        _root_.bit0, _root_.bit0, neg_add_rev]
id                         └─────────┘  └─────────┘  └─────────┘
src  ─────────────────────┘└─────────┘└┘└─────────┘└┘└─────────┘└─
typ  ─────────────────────┘└─────────┘└┘└─────────┘└┘└─────────┘└─
doc  ─────────────────────┘           └┘           └┘           └─
txt  ─────────────────────┘           └┘           └┘           └─
par  ─────────────────────┘           └┘           └┘           └─
pid  ─────────────────────┘           └┘           └┘           
st   ────────────────────────────────┘└───────────┘└───────────┘
728  
src  
typ  
doc  
txt  
par  
pid  
st   
729    @[simp] theorem cast_bit1 [add_group α] [has_one α] :
id                                └───────┘    └─────┘ 
src  ─┘                           └───────┘     └─────┘
typ  ─┘                           └───────┘    └─────┘ 
doc  ─┘  └──┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
730      ∀ n : znum, (n.bit1 : α) = bit1 n
id            └──┘   └───┘      └──┘ 
src            └──┘    └───┘       └──┘
typ           └──┘   └───┘      └──┘ 
doc            └──┘
731    | 0       := by simp [znum.bit1, _root_.bit1, _root_.bit0]
id                           └───────┘  └─────────┘  └─────────┘
src                    └────┘└───────┘└┘└─────────┘└┘└─────────┘└─
typ                    └────┘└───────┘└┘└─────────┘└┘└─────────┘└─
doc                    └────┘         └┘           └┘           └─
txt                    └────┘         └┘           └┘           └─
par                    └────┘         └┘           └┘           └─
pid                                 └┘           └┘           
st                    └───────────────────────────────────────────
732    | (pos p) := by rw [znum.bit1, cast_pos, cast_pos]; refl
id        └─┘              └───────┘  └──────┘  └──────┘
src  ─┘   └─┘          └──┘└───────┘└┘└──────┘└┘└──────┘  └────
typ  ─┘   └─┘          └──┘└───────┘└┘└──────┘└┘└──────┘  └────
doc  ─┘                └──┘         └┘        └┘          └────
txt  ─┘                └──┘         └┘        └┘          └────
par  ─┘                └──┘         └┘        └┘          └────
pid  ─┘                  └┘         └┘        └┘              
st   ─┘               └────────────┘└────────┘└────────┘└──────
733    | (neg p) := begin
id        └─┘
src  ─┘   └─┘
typ  ─┘   └─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘             └─────
734        rw [znum.bit1, cast_neg, cast_neg],
id             └───────┘  └──────┘  └──────┘
src        └──┘└───────┘└┘└──────┘└┘└──────┘
typ        └──┘└───────┘└┘└──────┘└┘└──────┘
doc        └──┘         └┘        └┘        
txt        └──┘         └┘        └┘        
par        └──┘         └┘        └┘        
pid          └┘         └┘        └┘        
st   ──────────────────┘└────────┘└────────┘
735        cases e : pred' p;
id                   └───┘ 
src                  └───┘
typ                  └───┘ 
736        have : p = _ := (succ'_pred' p).symm.trans
id                                     
typ                                    
737          (congr_arg num.succ' e),
id                      └───────┘
src                     └───────┘
typ                     └───────┘
738        { change p=1 at this, subst p,
id                                    
typ                                   
739          simp [_root_.bit1, _root_.bit0] },
st                                           └┘
740        { rw [num.succ'] at this, subst p,
id                                         
typ                                        
741          have : (↑(-↑a:ℤ) : α) = -1 + ↑(-↑a + 1 : ℤ), {simp},
id                                           
typ                                          
st                                                             └┘
742          simpa [_root_.bit1, _root_.bit0, -add_comm] },
st                                                       └┘
743      end
st       └─┘
744  
745    @[simp] theorem cast_bitm1 [add_group α] [has_one α]
id                                 └──┘  └─┘     └┘ └┘  
src                                └──┘  └─┘      └┘ └┘
typ                                └──┘  └─┘     └┘ └┘  
doc      └──┘
746      (n : znum) : (n.bitm1 : α) = bit0 n - 1 :=
id            └──┘     └─┘              
src           └──┘      └─┘  
typ           └──┘     └─┘              
doc           └──┘
747    begin
748      conv { to_lhs, rw ← zneg_zneg n },
id                                     
typ                                    
749      rw [← zneg_bit1, cast_zneg, cast_bit1],
750      have : ((-1 + n + n : ℤ) : α) = (n + n + -1 : ℤ), {simp},
id                                          
src                            
typ                                         
st                                                              └┘
751      simpa [_root_.bit1, _root_.bit0, -add_comm]
752    end
st     └─┘
753  
754    theorem add_zero (n : znum) : n + 0 = n := by cases n; refl
id                           └──┘                           └──┘
src                          └──┘                             └──┘
typ                          └──┘                           └──┘
doc                          └──┘                             └──┘
755    theorem zero_add (n : znum) : 0 + n = n := by cases n; refl
id                           └──┘                           └──┘
src                          └──┘                             └──┘
typ                          └──┘                           └──┘
doc                          └──┘                             └──┘
756  
757    theorem add_one : ∀ n : znum, n + 1 = succ n
id                             └──┘            
src                            └──┘            
typ                            └──┘            
doc                            └──┘
758    | 0       := rfl
759    | (pos p) := congr_arg pos p.add_one
id                           
src                           
typ                          
760    | (neg p) := by cases p; refl
id        └─┘                  └──┘
src       └─┘                   └──┘
typ       └─┘                  └──┘
doc                             └──┘
761  
762  end znum
763  
764  namespace pos_num
765    variables {α : Type*}
766  
767    theorem cast_to_znum : ∀ n : pos_num, (n : znum) = znum.pos n
id                                  └─────┘      └──┘      └┘   
src                                 └─────┘       └──┘      └┘  
typ                                 └─────┘      └──┘      └┘   
doc                                 └─────┘       └──┘
768    | 1        := rfl
769    | (bit0 p) := (znum.bit0_of_bit0 p).trans $ congr_arg _ (cast_to_znum p)
id          └┘ 
src         └┘
typ         └┘ 
770    | (bit1 p) := (znum.bit1_of_bit1 p).trans $ congr_arg _ (cast_to_znum p)
id         └─┘ 
src        └─┘
typ        └─┘ 
771  
772    theorem cast_sub' [add_group α] [has_one α] : ∀ m n : pos_num, (sub' m n : α) = m - n
id                        └──┘  └─┘      └─┘              └────┘                   
src                       └──┘  └─┘       └─┘               └────┘
typ                       └──┘  └─┘      └─┘              └────┘                   
doc                                                           └────┘
773    | a        1        := by rw [sub'_one, num.cast_to_znum,
774                                  ← num.cast_to_nat, pred'_to_nat, ← nat.sub_one];
775                              simp [pos_num.cast_pos]
776    | 1        b        := by rw [one_sub', num.cast_to_znum_neg, ← neg_sub, neg_inj',
777                                  ← num.cast_to_nat, pred'_to_nat, ← nat.sub_one];
778                              simp [pos_num.cast_pos]
779    | (bit0 a) (bit0 b) := begin
id                 └──┘
src                └──┘
typ                └──┘
780        rw [sub', znum.cast_bit0, cast_sub'],
781        have : ((a + -b + (a + -b) : ℤ) : α) = a + a + (-b + -b), {simp},
id                                                             
typ                                                            
st                                                                        └┘
782        simpa [_root_.bit0, -add_left_comm]
783      end
st       └─┘
784    | (bit0 a) (bit1 b) := begin
id        └──┘     └──┘
src       └──┘     └──┘
typ       └──┘     └──┘
785        rw [sub', znum.cast_bitm1, cast_sub'],
786        have : ((-b + (a + (-b + -1)) : ℤ) : α) = (a + -1 + (-b + -b):ℤ), {simp},
id                                                                  
typ                                                                 
st                                                                                └┘
787        simpa [_root_.bit1, _root_.bit0, -add_left_comm, -add_comm]
788      end
st       └─┘
789    | (bit1 a) (bit0 b) := begin
id        └──┘     └──┘
src       └──┘     └──┘
typ       └──┘     └──┘
790        rw [sub', znum.cast_bit1, cast_sub'],
791        have : ((-b + (a + (-b + 1)) : ℤ) : α) = (a + 1 + (-b + -b):ℤ), {simp},
id                                                                
typ                                                               
st                                                                              └┘
792        simpa [_root_.bit1, _root_.bit0, -add_left_comm, -add_comm]
793      end
st       └─┘
794    | (bit1 a) (bit1 b) := begin
id                 └──┘
src                └──┘
typ                └──┘
795        rw [sub', znum.cast_bit0, cast_sub'],
796        have : ((-b + (a + -b) : ℤ) : α) = a + (-b + -b), {simp},
id                                                     
typ                                                    
st                                                                └┘
797        simpa [_root_.bit1, _root_.bit0, -add_left_comm, add_neg_cancel_left]
798      end
st       └─┘
799  
800    theorem to_nat_eq_succ_pred (n : pos_num) : (n:ℕ) = n.pred' + 1 :=
id                                      └─────┘          └┘ └─┘
src                                     └─────┘            └┘ └─┘
typ                                     └─────┘          └┘ └─┘
doc                                     └─────┘
801    by rw [← num.succ'_to_nat, n.succ'_pred']
802  
803    theorem to_int_eq_succ_pred (n : pos_num) : (n:ℤ) = (n.pred' : ℕ) + 1 :=
id                                      └─────┘           └─┘ └┘   
src                                     └─────┘             └─┘ └┘   
typ                                     └─────┘           └─┘ └┘   
doc                                     └─────┘
804    by rw [← n.to_nat_to_int, to_nat_eq_succ_pred]; refl
id                                                     └──┘
src                                                    └──┘
typ                                                    └──┘
doc                                                    └──┘
805  
806  end pos_num
807  
808  namespace num
809    variables {α : Type*}
810  
811    @[simp] theorem cast_sub' [add_group α] [has_one α] : ∀ m n : num, (sub' m n : α) = m - n
id                                └┘  └──┘      └┘ └┘             └─┘                   
src                               └┘  └──┘       └┘ └┘              └─┘
typ                               └┘  └──┘      └┘ └┘             └─┘                   
doc      └──┘                                                        └─┘
812    | 0       0       := (sub_zero _).symm
813    | (pos a) 0       := (sub_zero _).symm
id         
src        
typ        
814    | 0       (pos b) := (zero_sub _).symm
id                └┘
src               └┘
typ               └┘
815    | (pos a) (pos b) := pos_num.cast_sub' _ _
id                 
src                
typ                
816  
817    @[simp] theorem of_nat_to_znum : ∀ n : ℕ, to_znum n = n
id                                              └┘  └┘     
src                                             └┘  └┘
typ                                             └┘  └┘     
doc      └──┘
818    | 0     := rfl
819    | (n+1) := by rw [nat.cast_add_one, nat.cast_add_one,
820      znum.add_one, add_one, ← of_nat_to_znum]; cases (n:num); refl
id                                                         └─┘   └──┘
src                                                         └─┘   └──┘
typ                                                        └─┘   └──┘
doc                                                         └─┘   └──┘
821  
822    @[simp] theorem of_nat_to_znum_neg (n : ℕ) : to_znum_neg n = -n :=
id                                                 └┘  └┘  └┘      
src                                                └┘  └┘  └┘
typ                                                └┘  └┘  └┘      
doc      └──┘
823    by rw [← of_nat_to_znum, zneg_to_znum]
824  
825    theorem mem_of_znum' : ∀ {m : num} {n : znum}, m ∈ of_znum' n ↔ n = to_znum m
id                                   └─┘       └──┘                     └┘  └┘  
src                                  └─┘       └──┘                        └┘  └┘
typ                                  └─┘       └──┘                     └┘  └┘  
doc                                  └─┘       └──┘
826    | 0       0      := ⟨λ _, rfl, λ _, rfl⟩
827    | (pos m) 0      := ⟨λ h, by cases h, λ h, by cases h⟩
id         
src        
typ        
828    | m (znum.pos p) := option.some_inj.trans $
id          └──────┘
src         └──────┘
typ         └──────┘
829      by cases m; split; intro h; try {cases h}; refl
id                  └───┘           └─┘            └──┘
src                  └───┘           └─┘            └──┘
typ                 └───┘           └─┘            └──┘
doc                  └───┘           └─┘            └──┘
830    | m (znum.neg p) := ⟨λ h, by cases h, λ h, by cases m; cases h⟩
id          └──────┘                                       
src         └──────┘
typ         └──────┘                                       
831  
832    theorem of_znum'_to_nat : ∀ (n : znum), coe <$> of_znum' n = int.to_nat' n
id                                      └──┘                                   
src                                     └──┘
typ                                     └──┘                                   
doc                                     └──┘
833    | 0            := rfl
834    | (znum.pos p) := show _ = int.to_nat' p, by rw [← pos_num.to_nat_to_int p]; refl
id          └┘  └┘                                                                 └──┘
src         └┘  └┘                                                                  └──┘
typ         └┘  └┘                                                                 └──┘
doc                                                                                 └──┘
835    | (znum.neg p) := congr_arg (λ x, int.to_nat' (-x)) $
id        └──────┘                                   
src       └──────┘
typ       └──────┘                                   
836      show ((p.pred' + 1 : ℕ) : ℤ) = p, by rw ← succ'_to_nat; simp
id               └────┘           
src              └────┘           
typ              └────┘           
837  
838    @[simp] theorem of_znum_to_nat : ∀ (n : znum), (of_znum n : ℕ) = int.to_nat n
id                                             └──┘      └┘          └┘  └┘  └┘ 
src                                            └──┘      └┘           └┘  └┘  └┘
typ                                            └──┘      └┘          └┘  └┘  └┘ 
doc      └──┘                                  └──┘
839    | 0            := rfl
840    | (znum.pos p) := show _ = int.to_nat p, by rw [← pos_num.to_nat_to_int p]; refl
id          └────┘               └─┘  └──┘                                        └──┘
src         └────┘                └─┘  └──┘                                        └──┘
typ         └────┘               └─┘  └──┘                                        └──┘
doc                                                                                └──┘
841    | (znum.neg p) := congr_arg (λ x, int.to_nat (-x)) $
id        └──────┘                     └────────┘   
src       └──────┘                       └────────┘
typ       └──────┘                     └────────┘   
842      show ((p.pred' + 1 : ℕ) : ℤ) = p, by rw ← succ'_to_nat; simp
id               └────┘           
src              └────┘           
typ              └────┘           
843  
844    @[simp] theorem cast_of_znum [add_group α] [has_one α] (n : znum) :
id                                   └──┘  └─┘     └┘ └┘         └──┘
src                                  └──┘  └─┘      └┘ └┘          └──┘
typ                                  └──┘  └─┘     └┘ └┘         └──┘
doc      └──┘                                                      └──┘
845      (of_znum n : α) = int.to_nat n :=
id         └┘  └┘          └┘  └┘  
src        └┘  └┘            └┘  └┘
typ        └┘  └┘          └┘  └┘  
846    by rw [← cast_to_nat, of_znum_to_nat]
847  
848    @[simp] theorem sub_to_nat (m n) : ((m - n : num) : ℕ) = m - n :=
id                                                └─┘           
src                                                 └─┘    
typ                                               └─┘           
doc      └──┘                                       └─┘
849    show (of_znum _ : ℕ) = _, by rw [of_znum_to_nat, cast_sub',
id            └┘  └┘     
src           └┘  └┘     
typ           └┘  └┘     
850      ← to_nat_to_int, ← to_nat_to_int, int.to_nat_sub]
st                                                       
851  
852  end num
853  
854  namespace znum
855    variables {α : Type*}
856  
857    @[simp] theorem cast_add [add_group α] [has_one α] : ∀ m n, ((m + n : znum) : α) = m + n
id                               └┘  └──┘      └┘ └┘                   └──┘           
src                              └┘  └──┘       └┘ └┘                       └──┘
typ                              └┘  └──┘      └┘ └┘                   └──┘           
doc      └──┘                                                                └──┘
858    | 0       a       := by cases a; exact (_root_.zero_add _).symm
id                                   
typ                                  
859    | b       0       := by cases b; exact (_root_.add_zero _).symm
id                                   
typ                                  
860    | (pos a) (pos b) := pos_num.cast_add _ _
id                └─┘
src               └─┘
typ               └─┘
861    | (pos a) (neg b) := pos_num.cast_sub' _ _
id        └─┘     └─┘
src       └─┘     └─┘
typ       └─┘     └─┘
862    | (neg a) (pos b) := (pos_num.cast_sub' _ _).trans $
id        └─┘    └─┘ 
src       └─┘     └─┘
typ       └─┘    └─┘ 
863      show ↑b + -↑a = -↑a + ↑b, by rw [← pos_num.cast_to_int a, ← pos_num.cast_to_int b,
id                                                                                      
typ                                                                                     
864        ← int.cast_neg, ← int.cast_add (-a)]; simp
id                                          
typ                                         
865    | (neg a) (neg b) := show -(↑(a + b) : α) = -a + -b, by rw [
id               └─┘                        
src               └─┘
typ              └─┘                        
866      pos_num.cast_add, neg_eq_iff_neg_eq, neg_add_rev, neg_neg, neg_neg,
867      ← pos_num.cast_to_int a, ← pos_num.cast_to_int b, ← int.cast_add]; simp
id                                                     
typ                                                    
868  
869    @[simp] theorem cast_succ [add_group α] [has_one α] (n) : ((succ n : znum) : α) = n + 1 :=
id                                └──┘  └─┘     └┘ └┘             └┘     └──┘        
src                               └──┘  └─┘      └┘ └┘              └┘      └──┘
typ                               └──┘  └─┘     └┘ └┘             └┘     └──┘        
doc      └──┘                                                               └──┘
870    by rw [← add_one, cast_add, cast_one]
st                                         
871  
872    @[simp] theorem mul_to_int : ∀ m n, ((m * n : znum) : ℤ) = m * n
id                                                └──┘           
src                                                  └──┘    
typ                                               └──┘           
doc      └──┘                                        └──┘
873    | 0       a       := by cases a; exact (_root_.zero_mul _).symm
id                                   
typ                                  
874    | b       0       := by cases b; exact (_root_.mul_zero _).symm
id                                   
typ                                  
875    | (pos a) (pos b) := pos_num.cast_mul a b
id               └─┘ 
src               └─┘
typ              └─┘ 
876    | (pos a) (neg b) := show -↑(a * b) = ↑a * -↑b, by rw [pos_num.cast_mul, neg_mul_eq_mul_neg]
id        └─┘    └─┘ 
src       └─┘     └─┘
typ       └─┘    └─┘ 
st                                                                                                
877    | (neg a) (pos b) := show -↑(a * b) = -↑a * ↑b, by rw [pos_num.cast_mul, neg_mul_eq_neg_mul]
id        └─┘    └─┘ 
src       └─┘     └─┘
typ       └─┘    └─┘ 
st                                                                                                
878    | (neg a) (neg b) := show ↑(a * b) = -↑a * -↑b, by rw [pos_num.cast_mul, neg_mul_neg]
id               └─┘ 
src               └─┘
typ              └─┘ 
st                                                                                         
879  
880    theorem cast_mul [ring α] (m n) : ((m * n : znum) : α) = m * n :=
id                       └──┘                    └──┘           
src                      └──┘                      └──┘
typ                      └──┘                    └──┘           
doc                                                └──┘
881    by rw [← cast_to_int, mul_to_int, int.cast_mul, cast_to_int, cast_to_int]
st                                                                             
882  
883    @[simp] theorem of_to_int : Π (n : znum), ((n : ℤ) : znum) = n
id                                        └──┘            └──┘    
src                                       └──┘             └──┘
typ                                       └──┘            └──┘    
doc      └──┘                             └──┘              └──┘
884    | 0       := rfl
885    | (pos a) := by rw [cast_pos, ← pos_num.cast_to_nat,
id          
src         
typ         
886      int.cast_coe_nat', ← num.of_nat_to_znum, pos_num.of_to_nat]; refl
id                                                                    └──┘
src                                                                   └──┘
typ                                                                   └──┘
doc                                                                   └──┘
887    | (neg a) := by rw [cast_neg, neg_of_int, ← pos_num.cast_to_nat,
id        └─┘
src       └─┘
typ       └─┘
888      int.cast_coe_nat', ← num.of_nat_to_znum_neg, pos_num.of_to_nat]; refl
id                                                                        └──┘
src                                                                       └──┘
typ                                                                       └──┘
doc                                                                       └──┘
889  
890    @[simp] theorem to_of_int : Π (n : ℤ), ((n : znum) : ℤ) = n
id                                                └──┘        
src                                                └──┘    
typ                                               └──┘        
doc      └──┘                                       └──┘
891    | (n : ℕ) := by rw [int.cast_coe_nat,
id            
src           
typ           
892      ← num.of_nat_to_znum, num.cast_to_znum, ← num.cast_to_nat,
893      int.nat_cast_eq_coe_nat, num.to_of_nat]
st                                             
894    | -[1+ n] := by rw [int.cast_neg_succ_of_nat, cast_zneg,
id       └──┘
src      └──┘
typ      └──┘
895      add_one, cast_succ, int.neg_succ_of_nat_eq,
896      ← num.of_nat_to_znum, num.cast_to_znum, ← num.cast_to_nat,
897      int.nat_cast_eq_coe_nat, num.to_of_nat]
st                                             
898  
899    theorem to_int_inj {m n : znum} : (m : ℤ) = n ↔ m = n :=
id                               └──┘                 
src                              └──┘               
typ                              └──┘                 
doc                              └──┘
900    ⟨λ h, function.injective_of_left_inverse of_to_int h, congr_arg _⟩
901  
902    @[simp] theorem of_int_cast [add_group α] [has_one α] (n : ℤ) : ((n : znum) : α) = n :=
id                                    └──┘      └┘ └┘                   └──┘        
src                                   └──┘       └┘ └┘                     └──┘
typ                                   └──┘      └┘ └┘                   └──┘        
doc      └──┘                                                                └──┘
903    by rw [← cast_to_int, to_of_int]
904  
905    @[simp] theorem of_nat_cast [add_group α] [has_one α] (n : ℕ) : ((n : znum) : α) = n :=
id                                  └──┘  └─┘     └┘ └┘                  └──┘        
src                                 └──┘  └─┘      └┘ └┘                    └──┘
typ                                 └──┘  └─┘     └┘ └┘                  └──┘        
doc      └──┘                                                                └──┘
906    of_int_cast n
id                 
typ                
907  
908    @[simp] theorem of_int'_eq : ∀ n, znum.of_int' n = n
id                                        └┘  └┘  └┘     
src                                       └┘  └┘  └┘
typ                                       └┘  └┘  └┘     
doc      └──┘
909    | (n : ℕ) := to_int_inj.1 $ by simp [znum.of_int']
id                                         └──────────┘
src                                        └──────────┘
typ                                        └──────────┘
910    | -[1+ n] := to_int_inj.1 $ by simp [znum.of_int']
id       └──┘                               └──────────┘
src      └──┘                               └──────────┘
typ      └──┘                               └──────────┘
911  
912    theorem cmp_to_int : ∀ (m n), (ordering.cases_on (cmp m n) ((m:ℤ) < n) (m = n) ((m:ℤ) > n) : Prop)
id                                                                                  
src                                                                                      
typ                                                                                 
913    | 0       0       := rfl
914    | (pos a) (pos b) := begin
id                └─┘
src               └─┘
typ               └─┘
915        have := pos_num.cmp_to_nat a b; revert this; dsimp [cmp];
id                                                           └─┘
src                                                            └─┘
typ                                                          └─┘
916        cases pos_num.cmp a b; dsimp;
id               └─────────┘  
src              └─────────┘
typ              └─────────┘  
917        [simp, exact congr_arg pos, simp [gt]]
id                                └─┘
src                               └─┘
typ                               └─┘
918      end
st       └─┘
919    | (neg a) (neg b) := begin
id                └─┘
src               └─┘
typ               └─┘
920        have := pos_num.cmp_to_nat b a; revert this; dsimp [cmp];
id                                                           └─┘
src                                                            └─┘
typ                                                          └─┘
921        cases pos_num.cmp b a; dsimp;
id               └─────────┘  
src              └─────────┘
typ              └─────────┘  
922        [simp, simp {contextual := tt}, simp [gt]]
id                                    └┘
src                                   └┘
typ                                   └┘
923      end
st       └─┘
924    | (pos a) 0       := pos_num.cast_pos _
id        └─┘
src       └─┘
typ       └─┘
925    | (pos a) (neg b) := lt_trans (neg_lt_zero.2 $ pos_num.cast_pos _) (pos_num.cast_pos _)
id        └─┘     └─┘
src       └─┘     └─┘
typ       └─┘     └─┘
926    | 0       (neg b) := neg_lt_zero.2 $ pos_num.cast_pos _
id                └─┘
src               └─┘
typ               └─┘
927    | (neg a) 0       := neg_lt_zero.2 $ pos_num.cast_pos _
id        └─┘
src       └─┘
typ       └─┘
928    | (neg a) (pos b) := lt_trans (neg_lt_zero.2 $ pos_num.cast_pos _) (pos_num.cast_pos _)
id        └─┘     └─┘
src       └─┘     └─┘
typ       └─┘     └─┘
929    | 0       (pos b) := pos_num.cast_pos _
id                └─┘
src               └─┘
typ               └─┘
930  
931    @[simp] theorem lt_to_int {m n : znum} : (m:ℤ) < n ↔ m < n :=
id                                      └──┘               
src                                     └──┘             
typ                                     └──┘               
doc      └──┘                           └──┘
932    show (m:ℤ) < n ↔ cmp m n = ordering.lt, from
id                           └─────────┘
src                              └─────────┘
typ                          └─────────┘
933    match cmp m n, cmp_to_int m n with
id                              
typ                             
934    | ordering.lt, h := by simp at h; simp [h]
id       └─────────┘
src      └─────────┘
typ      └─────────┘
935    | ordering.eq, h := by simp at h; simp [h, lt_irrefl]; exact dec_trivial
id       └─────────┘                           
src      └─────────┘
typ      └─────────┘                           
936    | ordering.gt, h := by simp [not_lt_of_gt h]; exact dec_trivial
id       └─────────┘
src      └─────────┘
typ      └─────────┘
937    end
938  
939    @[simp] theorem le_to_int {m n : znum} : (m:ℤ) ≤ n ↔ m ≤ n :=
id                                      └──┘               
src                                     └──┘             
typ                                     └──┘               
doc      └──┘                           └──┘
940    by rw ← not_lt; exact not_congr lt_to_int
941  
942    @[simp] theorem cast_lt [linear_ordered_ring α] {m n : znum} : (m:α) < n ↔ m < n :=
id                              └──┘  └──┘  └──┘            └──┘               
src                             └──┘  └──┘  └──┘             └──┘              
typ                             └──┘  └──┘  └──┘            └──┘               
doc      └──┘                                                 └──┘
943    by rw [← cast_to_int m, ← cast_to_int n, int.cast_lt, lt_to_int]
st                                                                    
944  
945    @[simp] theorem cast_le [linear_ordered_ring α] {m n : znum} : (m:α) ≤ n ↔ m ≤ n :=
id                              └──┘  └──┘  └──┘            └──┘               
src                             └──┘  └──┘  └──┘             └──┘              
typ                             └──┘  └──┘  └──┘            └──┘               
doc      └──┘                                                 └──┘
946    by rw ← not_lt; exact not_congr cast_lt
947  
948    @[simp] theorem cast_inj [linear_ordered_ring α] {m n : znum} : (m:α) = n ↔ m = n :=
id                               └──┘  └──┘  └──┘            └──┘               
src                              └──┘  └──┘  └──┘             └──┘              
typ                              └──┘  └──┘  └──┘            └──┘               
doc      └──┘                                                  └──┘
949    by rw [← cast_to_int m, ← cast_to_int n, int.cast_inj, to_int_inj]
st                                                                      
950  
951    meta def transfer_rw : tactic unit :=
id                                   └──┘
src                                  └──┘
typ                                  └──┘
doc                                  └──┘
952    `[repeat {rw ← to_int_inj <|> rw ← lt_to_int <|> rw ← le_to_int},
953      repeat {rw cast_add <|> rw mul_to_int <|> rw cast_one <|> rw cast_zero}]
954  
955    meta def transfer : tactic unit := `[intros, transfer_rw, try {simp [mul_comm, mul_left_comm]}]
id                                └──┘
src                               └──┘
typ                               └──┘
doc                               └──┘
956  
957    instance : decidable_linear_order znum :=
id                └┘  └┘  └┘  └┘  └┘  └┘ └──┘
src               └┘  └┘  └┘  └┘  └┘  └┘ └──┘
typ               └┘  └┘  └┘  └┘  └┘  └┘ └──┘
doc                                      └──┘
958    { lt               := (<),
959      lt_iff_le_not_le := by {intros a b, transfer_rw, apply lt_iff_le_not_le},
st                                                                              └┘
960      le               := (≤),
961      le_refl          := by transfer,
962      le_trans         := by {intros a b c, transfer_rw, apply le_trans},
st                                                                        └┘
963      le_antisymm      := by {intros a b, transfer_rw, apply le_antisymm},
st                                                                         └┘
964      le_total         := by {intros a b, transfer_rw, apply le_total},
st                                                                      └┘
965      decidable_eq     := znum.decidable_eq,
id                           └───────────────┘
src                          └───────────────┘
typ                          └───────────────┘
966      decidable_le     := znum.decidable_le,
967      decidable_lt     := znum.decidable_lt }
968  
969    instance : add_comm_group znum :=
id                └┘  └┘  └┘  └┘ └──┘
src               └┘  └┘  └┘  └┘ └──┘
typ               └┘  └┘  └┘  └┘ └──┘
doc                              └──┘
970    { add              := (+),
971      add_assoc        := by transfer,
972      zero             := 0,
973      zero_add         := zero_add,
974      add_zero         := add_zero,
975      add_comm         := by transfer,
976      neg              := has_neg.neg,
977      add_left_neg     := by transfer }
978  
979    instance : decidable_linear_ordered_comm_ring znum :=
id                └┘  └┘  └┘  └┘  └┘  └┘  └┘  └┘  └┘ └──┘
src               └┘  └┘  └┘  └┘  └┘  └┘  └┘  └┘  └┘ └──┘
typ               └┘  └┘  └┘  └┘  └┘  └┘  └┘  └┘  └┘ └──┘
doc                                                  └──┘
980    { mul              := (*),
981      mul_assoc        := by transfer,
982      one              := 1,
983      one_mul          := by transfer,
984      mul_one          := by transfer,
985      left_distrib     := by {transfer, simp [mul_add]},
st                                                       └┘
986      right_distrib    := by {transfer, simp [mul_add, mul_comm]},
st                                                                 └┘
987      mul_comm         := by transfer,
988      zero_ne_one      := dec_trivial,
989      add_le_add_left  := by {intros a b h c, revert h, transfer_rw, exact λ h, add_le_add_left h c},
id                                                                                                   
typ                                                                                                  
st                                                                                                    └┘
990      add_lt_add_left  := by {intros a b h c, revert h, transfer_rw, exact λ h, add_lt_add_left h c},
id                                                                                                   
typ                                                                                                  
st                                                                                                    └┘
991      mul_pos          := by {intros a b, transfer_rw, apply mul_pos},
st                                                                     └┘
992      mul_nonneg       := by {intros x y,
993        change 0 ≤ x → 0 ≤ y → 0 ≤ x * y,
id                                       
typ                                      
994        transfer_rw, apply mul_nonneg},
st                                      └┘
995      zero_lt_one      := dec_trivial,
996      ..znum.decidable_linear_order, ..znum.add_comm_group }
id         └─────────────────────────┘    └─────────────────┘
src        └─────────────────────────┘    └─────────────────┘
typ        └─────────────────────────┘    └─────────────────┘
997  
998    @[simp] theorem dvd_to_int (m n : znum) : (m : ℤ) ∣ n ↔ m ∣ n :=
id                                       └──┘                 
src                                      └──┘               
typ                                      └──┘                 
doc      └──┘                            └──┘
999    ⟨λ ⟨k, e⟩, ⟨k, by rw [← of_to_int n, e]; simp⟩,
id         
typ        
1000     λ ⟨k, e⟩, ⟨k, by simp [e]⟩⟩
id         
typ        
1001  
1002  end znum
1003  
1004  namespace pos_num
1005  
1006    theorem divmod_to_nat_aux {n d : pos_num} {q r : num}
id                                      └─────┘         └─┘
src                                     └─────┘         └─┘
typ                                     └─────┘         └─┘
doc                                     └─────┘         └─┘
1007      (h₁ : (r:ℕ) + d * _root_.bit0 q = n)
id                                     
src               
typ                                    
1008      (h₂ : (r:ℕ) < 2 * d) :
id                       
src               
typ                      
1009      ((divmod_aux d q r).2 + d * (divmod_aux d q r).1 : ℕ) = ↑n ∧
id                                                        
src                                                         
typ                                                       
1010      ((divmod_aux d q r).2 : ℕ) < d :=
id                                
src                              
typ                               
1011    begin
1012      unfold divmod_aux,
1013      have : ∀ {r₂}, num.of_znum' (num.sub' r (num.pos d)) = some r₂ ↔ (r : ℕ) = r₂ + d,
id                 └┘   └──────────┘  └──────┘    └─────┘                              
src                     └──────────┘  └──────┘    └─────┘               
typ                └┘   └──────────┘  └──────┘    └─────┘                              
1014      { intro r₂,
1015        apply num.mem_of_znum'.trans,
1016        rw [← znum.to_int_inj, num.cast_to_znum,
1017          num.cast_sub', sub_eq_iff_eq_add, ← int.coe_nat_inj'],
1018        simp },
st              └┘
1019      cases e : num.of_znum' (num.sub' r (num.pos d)) with r₂;
id                 └──────────┘  └──────┘   └─────┘ 
src                └──────────┘  └──────┘    └─────┘
typ                └──────────┘  └──────┘   └─────┘ 
1020        simp [divmod_aux],
1021      { refine ⟨h₁, lt_of_not_ge (λ h, _)⟩,
1022        cases nat.le.dest h with r₂ e',
1023        rw [← num.to_of_nat r₂, add_comm] at e',
id                             └┘
typ                            └┘
1024        cases e.symm.trans (this.2 e'.symm) },
st                                             └┘
1025      { have := this.1 e,
1026        split,
1027        { rwa [_root_.bit1, add_comm _ 1, mul_add, mul_one,
1028            ← add_assoc, ← this] },
st                                  └┘
1029        { rwa [this, two_mul, add_lt_add_iff_right] at h₂ } }
st                                                           └──┘
1030    end
st     └─┘
1031  
1032    theorem divmod_to_nat (d n : pos_num) :
id                                  └─────┘
src                                 └─────┘
typ                                 └─────┘
doc                                 └─────┘
1033      (n / d : ℕ) = (divmod d n).1 ∧
id                               
src                                  
typ                              
1034      (n % d : ℕ) = (divmod d n).2 :=
id                           
src               
typ                          
1035    begin
1036      rw nat.div_mod_unique (pos_num.cast_pos _),
1037      induction n with n IH n IH,
id                 
typ                
1038      { exact divmod_to_nat_aux (by simp; refl)
id                                           └──┘
src                                          └──┘
typ                                          └──┘
doc                                          └──┘
1039          (nat.mul_le_mul_left 2
1040            (pos_num.cast_pos d : (0 : ℕ) < d)) },
id                               
typ                              
st                                                 └┘
1041      { unfold divmod,
1042        cases divmod d n with q r, simp only [divmod] at IH ⊢,
id                       
typ                      
1043        apply divmod_to_nat_aux; simp,
1044        { rw [_root_.bit1, _root_.bit1, add_right_comm,
1045            bit0_eq_two_mul ↑n, ← IH.1,
id                              
typ                             
1046            mul_add, ← bit0_eq_two_mul,
1047            mul_left_comm, ← bit0_eq_two_mul] },
st                                              └┘
1048        { rw ← bit0_eq_two_mul,
1049          exact nat.bit1_lt_bit0 IH.2 } },
st                                       └──┘
1050      { unfold divmod,
1051        cases divmod d n with q r, simp only [divmod] at IH ⊢,
id                       
typ                      
1052        apply divmod_to_nat_aux; simp,
1053        { rw [bit0_eq_two_mul ↑n, ← IH.1,
id                                
typ                               
1054            mul_add, ← bit0_eq_two_mul,
1055            mul_left_comm, ← bit0_eq_two_mul] },
st                                              └┘
1056        { rw ← bit0_eq_two_mul,
1057          exact nat.bit0_lt IH.2 } }
st                                  └──┘
1058    end
st     └─┘
1059  
1060    @[simp] theorem div'_to_nat (n d) : (div' n d : ℕ) = n / d :=
id                                                          
src                                                    
typ                                                         
doc      └──┘
1061    (divmod_to_nat _ _).1.symm
1062  
1063    @[simp] theorem mod'_to_nat (n d) : (mod' n d : ℕ) = n % d :=
id                                                          
src                                                    
typ                                                         
doc      └──┘
1064    (divmod_to_nat _ _).2.symm
1065  
1066  end pos_num
1067  
1068  namespace num
1069  
1070    @[simp] theorem div_to_nat : ∀ n d, ((n / d : num) : ℕ) = n / d
id                                                └─┘           
src                                                  └─┘    
typ                                               └─┘           
doc      └──┘                                        └─┘
1071    | 0       0       := rfl
1072    | 0       (pos d) := (nat.zero_div _).symm
id                └─┘
src               └─┘
typ               └─┘
1073    | (pos n) 0       := (nat.div_zero _).symm
id        └┘
src       └┘
typ       └┘
1074    | (pos n) (pos d) := pos_num.div'_to_nat _ _
id                 
src                
typ                
1075  
1076    @[simp] theorem mod_to_nat : ∀ n d, ((n % d : num) : ℕ) = n % d
id                                                └─┘           
src                                                  └─┘    
typ                                               └─┘           
doc      └──┘                                        └─┘
1077    | 0       0       := rfl
1078    | 0       (pos d) := (nat.zero_mod _).symm
id                └─┘
src               └─┘
typ               └─┘
1079    | (pos n) 0       := (nat.mod_zero _).symm
id        └┘
src       └┘
typ       └┘
1080    | (pos n) (pos d) := pos_num.mod'_to_nat _ _
id                 
src                
typ                
1081  
1082    theorem gcd_to_nat_aux : ∀ {n} {a b : num},
id                                          └─┘
src                                          └─┘
typ                                         └─┘
doc                                          └─┘
1083      a ≤ b → (a * b).nat_size ≤ n → (gcd_aux n a b : ℕ) = nat.gcd a b
id                  └┘  └┘                                    
src                     └┘  └┘                           
typ                 └┘  └┘                                    
1084    | 0            0       b       ab h := (nat.gcd_zero_left _).symm
1085    | 0            (pos a) 0       ab h := (not_lt_of_ge ab).elim rfl
id                     └─┘
src                    └─┘
typ                    └─┘
1086    | 0            (pos a) (pos b) ab h :=
id                             └─┘
src                            └─┘
typ                            └─┘
1087      (not_lt_of_le h).elim $ pos_num.nat_size_pos _
1088    | (nat.succ n) 0       b       ab h := (nat.gcd_zero_left _).symm
id        └──────┘
src       └──────┘
typ       └──────┘
1089    | (nat.succ n) (pos a) b       ab h := begin
id        └──────┘     └─┘
src       └──────┘     └─┘
typ       └──────┘     └─┘
1090      simp [gcd_aux],
id             └─────┘
src            └─────┘
typ            └─────┘
1091      rw [nat.gcd_rec, gcd_to_nat_aux, mod_to_nat], {refl},
st                                                          └┘
1092      { rw [← le_to_nat, mod_to_nat],
1093        exact le_of_lt (nat.mod_lt _ (pos_num.cast_pos _)) },
st                                                            └┘
1094      rw [nat_size_to_nat, mul_to_nat, nat.size_le] at h ⊢,
1095      rw [mod_to_nat, mul_comm],
1096      rw [nat.pow_succ, ← nat.mod_add_div b (pos a)] at h,
id                                             └─┘ 
src                                             └─┘
typ                                            └─┘ 
1097      refine lt_of_mul_lt_mul_right (lt_of_le_of_lt _ h) (nat.zero_le 2),
1098      rw [mul_two, mul_add],
1099      refine add_le_add_left (nat.mul_le_mul_left _
1100        (le_trans (le_of_lt (nat.mod_lt _ (pos_num.cast_pos _))) _)) _,
1101      suffices : 1 ≤ _, simpa using nat.mul_le_mul_left (pos a) this,
id                                                          └─┘ 
src                                                         └─┘
typ                                                         └─┘ 
1102      rw [nat.le_div_iff_mul_le _ _ a.cast_pos, one_mul],
1103      exact le_to_nat.2 ab
id                         └┘
typ                        └┘
1104    end
st     └─┘
1105  
1106    @[simp] theorem gcd_to_nat : ∀ a b, (gcd a b : ℕ) = nat.gcd a b :=
id                                                             
src                                                   
typ                                                            
doc      └──┘
1107    have ∀ a b : num, (a * b).nat_size ≤ a.nat_size + b.nat_size,
id                  └─┘       └──────┘    └─┘  └──┘   └┘  └───┘
src                 └─┘         └──────┘     └─┘  └──┘    └┘  └───┘
typ                 └─┘       └──────┘    └─┘  └──┘   └┘  └───┘
doc                 └─┘
1108    begin
1109      intros,
1110      simp [nat_size_to_nat],
1111      rw [nat.size_le, nat.pow_add],
1112      exact mul_lt_mul'' (nat.lt_size_self _)
1113        (nat.lt_size_self _) (nat.zero_le _) (nat.zero_le _)
1114    end,
st     └─┘
1115    begin
1116      intros, unfold gcd, split_ifs,
1117      { exact gcd_to_nat_aux h (this _ _) },
id                              
typ                             
st                                           └┘
1118      { rw nat.gcd_comm,
1119        exact gcd_to_nat_aux (le_of_not_le h) (this _ _) }
id                                            
typ                                           
st                                                          └┘
1120    end
st     └─┘
1121  
1122    theorem dvd_iff_mod_eq_zero {m n : num} : m ∣ n ↔ n % m = 0 :=
id                                        └─┘            
src                                       └─┘          
typ                                       └─┘            
doc                                       └─┘
1123    by rw [← dvd_to_nat, nat.dvd_iff_mod_eq_zero,
1124      ← to_nat_inj, mod_to_nat]; refl
id                                  └──┘
src                                 └──┘
typ                                 └──┘
doc                                 └──┘
1125  
1126    instance : decidable_rel ((∣) : num → num → Prop)
id                                     └─┘   └─┘
src                                    └─┘   └─┘
typ                                    └─┘   └─┘
doc                                    └─┘   └─┘
1127    | a b := decidable_of_iff' _ dvd_iff_mod_eq_zero
1128  
1129  end num
1130  
1131  namespace znum
1132  
1133    @[simp] theorem div_to_int : ∀ n d, ((n / d : znum) : ℤ) = n / d
id                                                └──┘           
src                                                  └──┘    
typ                                               └──┘           
doc      └──┘                                        └──┘
1134    | 0       0       := rfl
1135    | 0       (pos d) := (int.zero_div _).symm
id                └─┘
src               └─┘
typ               └─┘
1136    | 0       (neg d) := (int.zero_div _).symm
id                └┘
src               └┘
typ               └┘
1137    | (pos n) 0       := (int.div_zero _).symm
id         
src        
typ        
1138    | (neg n) 0       := (int.div_zero _).symm
id        └─┘
src       └─┘
typ       └─┘
1139    | (pos n) (pos d) := (num.cast_to_znum _).trans $
id                └─┘
src               └─┘
typ               └─┘
1140      by rw ← num.to_nat_to_int; simp
1141    | (pos n) (neg d) := (num.cast_to_znum_neg _).trans $
id        └─┘     └─┘
src       └─┘     └─┘
typ       └─┘     └─┘
1142      by rw ← num.to_nat_to_int; simp
1143    | (neg n) (pos d) := show - _ = (-_/↑d), begin
id        └─┘     └─┘ 
src       └─┘     └─┘
typ       └─┘     └─┘ 
1144        rw [n.to_int_eq_succ_pred, d.to_int_eq_succ_pred,
1145          ← pos_num.to_nat_to_int, num.succ'_to_nat,
1146          num.div_to_nat],
1147        change -[1+ n.pred' / ↑d] = -[1+ n.pred' / (d.pred' + 1)],
id                                          └─────┘    └─────┘
src                                         └─────┘    └─────┘
typ                                         └─────┘    └─────┘
1148        rw d.to_nat_eq_succ_pred
1149      end
st       └─┘
1150    | (neg n) (neg d) := show ↑(pos_num.pred' n / num.pos d).succ' = (-_ / -↑d), begin
id               └─┘             └───────────┘     └─────┘   └───┘
src               └─┘              └───────────┘     └─────┘   └───┘
typ              └─┘             └───────────┘     └─────┘   └───┘
1151        rw [n.to_int_eq_succ_pred, d.to_int_eq_succ_pred,
1152          ← pos_num.to_nat_to_int, num.succ'_to_nat,
1153          num.div_to_nat],
1154        change (nat.succ (_/d) : ℤ) = nat.succ (n.pred'/(d.pred' + 1)),
id                                       └──────┘  └─────┘  └─────┘
src                                      └──────┘  └─────┘  └─────┘
typ                                      └──────┘  └─────┘  └─────┘
1155        rw d.to_nat_eq_succ_pred
1156      end
st       └─┘
1157  
1158    @[simp] theorem mod_to_int : ∀ n d, ((n % d : znum) : ℤ) = n % d
id                                                └──┘           
src                                                  └──┘    
typ                                               └──┘           
doc      └──┘                                        └──┘
1159    | 0       d := (int.zero_mod _).symm
1160    | (pos n) d := (num.cast_to_znum _).trans $
id        └┘
src       └┘
typ       └┘
1161      by rw [← num.to_nat_to_int, cast_pos, num.mod_to_nat,
1162        ← pos_num.to_nat_to_int, abs_to_nat]; refl
id                                               └──┘
src                                              └──┘
typ                                              └──┘
doc                                              └──┘
1163    | (neg n) d := (num.cast_sub' _ _).trans $
id        └─┘ 
src       └─┘
typ       └─┘ 
1164      by rw [← num.to_nat_to_int, cast_neg, ← num.to_nat_to_int,
1165        num.succ_to_nat, num.mod_to_nat, abs_to_nat,
1166        ← int.sub_nat_nat_eq_coe, n.to_int_eq_succ_pred]; refl
id                                                           └──┘
src                                                          └──┘
typ                                                          └──┘
doc                                                          └──┘
1167  
1168    @[simp] theorem gcd_to_nat (a b) : (gcd a b : ℕ) = int.gcd a b :=
id                                                              
src                                                  
typ                                                             
doc      └──┘
1169    (num.gcd_to_nat _ _).trans $ by simpa
1170  
1171    theorem dvd_iff_mod_eq_zero {m n : znum} : m ∣ n ↔ n % m = 0 :=
id                                        └──┘            
src                                       └──┘          
typ                                       └──┘            
doc                                       └──┘
1172    by rw [← dvd_to_int, int.dvd_iff_mod_eq_zero,
1173      ← to_int_inj, mod_to_int]; refl
id                                  └──┘
src                                 └──┘
typ                                 └──┘
doc                                 └──┘
1174  
1175    instance : decidable_rel ((∣) : znum → znum → Prop)
id                                     └──┘   └──┘
src                                    └──┘   └──┘
typ                                    └──┘   └──┘
doc                                    └──┘   └──┘
1176    | a b := decidable_of_iff' _ dvd_iff_mod_eq_zero
1177  
1178  end znum